1 files changed, 50 insertions, 0 deletions
diff --git a/src/Cfe/Judgement/Properties.agda b/src/Cfe/Judgement/Properties.agda
index b5183eb..101994b 100644
--- a/src/Cfe/Judgement/Properties.agda
+++ b/src/Cfe/Judgement/Properties.agda
@@ -19,6 +19,56 @@ open import Data.Vec.Properties
 open import Function
 open import Relation.Binary.PropositionalEquality
 
+≅-refl : ∀ {a A m} {xs : Vec {a} A m} → xs ≅ xs
+≅-refl {xs = []} = []≅[]
+≅-refl {xs = x ∷ xs} = refl ∷ ≅-refl
+
+≅-reflexive : ∀ {a A m} {xs : Vec {a} A m} {ys} → xs ≡ ys → xs ≅ ys
+≅-reflexive refl = ≅-refl
+
+≅-length : ∀ {a A m n} {xs : Vec {a} A m} {ys : Vec _ n} → xs ≅ ys → m ≡ n
+≅-length []≅[] = refl
+≅-length (_ ∷ xs≅ys) = cong suc (≅-length xs≅ys)
+
+≅⇒≡ : ∀ {a A m n} {xs : Vec {a} A m} {ys : Vec _ n} → (xs≅ys : xs ≅ ys) → vcast (≅-length xs≅ys) xs ≡ ys
+≅⇒≡ []≅[] = refl
+≅⇒≡ (x≡y ∷ xs≅ys) = cong₂ _∷_ x≡y (≅⇒≡ xs≅ys)
+
+++ˡ : ∀ {a A m n k} {xs : Vec {a} A m} {ys : Vec _ n} (zs : Vec _ k) → xs ≅ ys → zs ++ xs ≅ zs ++ ys
+++ˡ [] xs≅ys = xs≅ys
+++ˡ (z ∷ zs) xs≅ys = refl ∷ ++ˡ zs xs≅ys
+
+cast₁ : ∀ {m₁ m₂ n} {Γ₁ : Vec _ m₁} {Γ₂ : Vec _ m₂} {Δ : Vec _ n} {e τ} → (eq : Γ₁ ≅ Γ₂) → Γ₁ , Δ ⊢ e ∶ τ → Γ₂ , Δ ⊢ cast (cong (n ℕ.+_) (≅-length eq)) e ∶ τ
+cast₁ eq Eps = Eps
+cast₁ eq (Char c) = Char c
+cast₁ eq Bot = Bot
+cast₁ {n = n} {Γ₁} {Δ = Δ} eq (Var {i = i} i≥n) =
+  subst₂ (_, Δ ⊢ cast (cong (n ℕ.+_) (≅-length eq)) (Var i) ∶_)
+         (≅⇒≡ eq)
+         (eq′ Γ₁ i≥n (≅-length eq))
+         (Var (ge (≅-length eq) i≥n))
+  where
+  open import Data.Empty using (⊥-elim)
+  open import Data.Fin.Properties using (toℕ<n; toℕ-cast; toℕ-injective)
+  open import Data.Nat.Properties using (<⇒≱; +-identityʳ; module ≤-Reasoning)
+
+  ge : ∀ {m₁ m₂ n i} → .(eq : m₁ ≡ m₂) → toℕ {n ℕ.+ m₁} i ≥ n → toℕ (F.cast (cong (n ℕ.+_) eq) i) ≥ n
+  ge {n = ℕ.zero} {i} _ _ = z≤n
+  ge {n = suc n} {suc i} eq (s≤s i≥n) = s≤s (ge eq i≥n)
+
+  eq′ : ∀ {a A m₁ m₂ n i} Γ i≥n → (eq : m₁ ≡ m₂) → lookup {a} {A} {m₂} (vcast eq Γ) (reduce≥ {n} (F.cast (cong (n ℕ.+_) eq) i) (ge eq i≥n)) ≡ lookup Γ (reduce≥ i i≥n)
+  eq′ {m₁ = ℕ.zero} {ℕ.zero} {n} {i} Γ i≥n _ = ⊥-elim (<⇒≱ (begin-strict
+    toℕ i <⟨ toℕ<n i ⟩
+    n ℕ.+ 0 ≡⟨ +-identityʳ n ⟩
+    n ∎) i≥n)
+    where
+    open ≤-Reasoning
+  eq′ {m₁ = suc m₁} {suc m₁} {ℕ.zero} {i} Γ i≥n refl = cong₂ lookup {vcast refl Γ} (≅⇒≡ ≅-refl) (toℕ-injective (toℕ-cast refl i))
+  eq′ {m₁ = suc m₁} {suc m₂} {suc n} {suc i} Γ (s≤s i≥n) eq = eq′ Γ i≥n eq
+cast₁ eq (Fix Γ₁,τ∷Δ⊢e∶τ) = Fix (cast₁ eq Γ₁,τ∷Δ⊢e∶τ)
+cast₁ {Δ = Δ} eq (Cat Γ₁,Δ⊢e₁∶τ₁ Δ++Γ₁,∙⊢e₂∶τ₂ τ₁⊛τ₂) = Cat (cast₁ eq Γ₁,Δ⊢e₁∶τ₁) (cast₁ (++ˡ Δ eq) Δ++Γ₁,∙⊢e₂∶τ₂) τ₁⊛τ₂
+cast₁ eq (Vee Γ₁,Δ⊢e₁∶τ₁ Γ₁,Δ⊢e₂∶τ₂ τ₁#τ₂) = Vee (cast₁ eq Γ₁,Δ⊢e₁∶τ₁) (cast₁ eq Γ₁,Δ⊢e₂∶τ₂) τ₁#τ₂
+
 wkn₁ : ∀ {m n} {Γ : Vec (Type ℓ ℓ) m} {Δ : Vec (Type ℓ ℓ) n} {e τ} →
        Γ , Δ ⊢ e ∶ τ →
        ∀ τ′ i →