diff options
| author | Chloe Brown <chloe.brown.00@outlook.com> | 2021-03-27 14:50:17 +0000 |
|---|---|---|
| committer | Chloe Brown <chloe.brown.00@outlook.com> | 2021-03-27 14:50:17 +0000 |
| commit | b254d61d3a4084e0f2dc47cded5b4482cc31ae23 (patch) | |
| tree | 2064ad4a0c54cdef923d6c42f4effae67498ad50 /src/Cfe/Context | |
| parent | a95622ca33a31a8c6d3cb31c7ca3b390e7aa5624 (diff) | |
Prove soundness of judgement.soundness
Diffstat (limited to 'src/Cfe/Context')
| -rw-r--r-- | src/Cfe/Context/Properties.agda | 5 |
1 files changed, 5 insertions, 0 deletions
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) |