From b254d61d3a4084e0f2dc47cded5b4482cc31ae23 Mon Sep 17 00:00:00 2001 From: Chloe Brown Date: Sat, 27 Mar 2021 14:50:17 +0000 Subject: Prove soundness of judgement. --- src/Cfe/Context/Properties.agda | 5 +++++ 1 file changed, 5 insertions(+) (limited to 'src/Cfe/Context') diff --git a/src/Cfe/Context/Properties.agda b/src/Cfe/Context/Properties.agda index b3037b2..42792d4 100644 --- a/src/Cfe/Context/Properties.agda +++ b/src/Cfe/Context/Properties.agda @@ -115,3 +115,8 @@ shift≤-wkn₂-comm-> record { m = m ; m≤n = m≤n ; Γ = Γ ; Δ = Δ } i≤ insert (take′ j≤m ys) (fromℕ< (s≤s i≤j)) y eq₂ {i = zero} _ _ _ _ _ = refl eq₂ {i = suc _} (x ∷ ys) (s≤s m≤n) (s≤s i≤j) (s≤s j≤m) y = cong (x ∷_) (eq₂ ys m≤n i≤j j≤m y) + +shift≤-toVec : ∀ {n i} (Γ,Δ : Context n) (i≤m : i ℕ.≤ _) → toVec (shift≤ Γ,Δ i≤m) ≡ toVec Γ,Δ +shift≤-toVec record { m = .0 ; m≤n = z≤n ; Γ = Γ ; Δ = [] } z≤n = refl +shift≤-toVec {suc n} record { m = .(suc _) ; m≤n = (s≤s m≤n) ; Γ = Γ ; Δ = (x ∷ Δ) } z≤n = cong (x ∷_) (shift≤-toVec (record { m≤n = m≤n ; Γ = Γ ; Δ = Δ }) z≤n) +shift≤-toVec {suc n} record { m = .(suc _) ; m≤n = (s≤s m≤n) ; Γ = Γ ; Δ = (x ∷ Δ) } (s≤s i≤m) = cong (x ∷_) (shift≤-toVec (record { m≤n = m≤n ; Γ = Γ ; Δ = Δ }) i≤m) -- cgit v1.2.3