From 06010ac93ef580440bbfda9d2b4ceba4baad211e Mon Sep 17 00:00:00 2001
From: Jad Ghalayini <jad.ghalayini@protonmail.com>
Date: Fri, 26 Jul 2024 00:51:59 +0100
Subject: [PATCH] Sad

---
 .../Rewrite/Region/Compose/Elgot.lean         |  59 +++--
 DeBruijnSSA/BinSyntax/Rewrite/Region/Eqv.lean | 202 ++++++++++++++++--
 .../BinSyntax/Rewrite/Region/LSubst.lean      |  15 +-
 .../BinSyntax/Rewrite/Region/Setoid.lean      |   5 +-
 DeBruijnSSA/BinSyntax/Rewrite/Term/Eqv.lean   |   6 +
 DeBruijnSSA/BinSyntax/Typing/LCtx.lean        |  42 ++++
 .../BinSyntax/Typing/Region/Basic.lean        |  37 ++--
 .../BinSyntax/Typing/Region/LSubst.lean       |   4 +
 DeBruijnSSA/BinSyntax/Typing/Term/Basic.lean  |   5 +-
 9 files changed, 312 insertions(+), 63 deletions(-)

diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Elgot.lean b/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Elgot.lean
index d1447c7..0700ba2 100644
--- a/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Elgot.lean
+++ b/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Elgot.lean
@@ -111,25 +111,19 @@ theorem Eqv.seq_cfg {A B C : Ty α} {Γ : Ctx α ε} {L : LCtx α}
   (G : ∀i : Fin R.length, Eqv φ (⟨R.get i, ⊥⟩::Γ) (R ++ C::L))
   : f ;; cfg R g (λi => (G i).vwk1)
   = cfg R
-    ((f.lwk sorry ;; g.cast rfl output_reshuffle_helper).cast rfl output_reshuffle_helper.symm)
+    ((f.lwk LCtx.InS.shf.slift ;; g.shf).ushf)
     (λi => (G i).vwk1)
-  := sorry
-
-theorem Eqv.seq_cont {A B C : Ty α} {Γ : Ctx α ε} {L : LCtx α}
-  (f : Eqv φ (⟨A, ⊥⟩::Γ) (B::L)) (g : Eqv φ (⟨B, ⊥⟩::Γ) (C::D::L))
-  (h : Eqv φ (⟨C, ⊥⟩::Γ) (C::D::L))
-  : f ;; cfg [C] g (Fin.elim1 h.vwk1) = cfg [C] (f.lwk1 ;; g) (Fin.elim1 h.vwk1)
   := by
   induction f using Eqv.arrow_induction with
-  | br ℓ a hℓ =>
+  | br ℓ a hl =>
     cases ℓ with
     | zero =>
       simp only [List.append_eq, List.nil_append, br_zero_eq_ret, wk_res_self, lwk1_ret, ret_seq,
         List.length_singleton, List.get_eq_getElem, List.singleton_append, vwk1_cfg, vsubst_cfg]
       congr
+      sorry
       funext i
-      cases i using Fin.elim1
-      induction h using Quotient.inductionOn
+      induction (G i) using Quotient.inductionOn
       induction a using Quotient.inductionOn
       apply Eqv.eq_of_reg_eq
       simp only [Set.mem_setOf_eq, InS.coe_vwk, Ctx.InS.coe_wk1, Fin.isValue, Fin.val_zero,
@@ -139,21 +133,44 @@ theorem Eqv.seq_cont {A B C : Ty α} {Γ : Ctx α ε} {L : LCtx α}
       congr
       funext i
       cases i <;> rfl
-    | succ ℓ => simp [cfg_br_ge]
+    | succ ℓ => sorry
   | let1 a r Ir =>
-    apply Eq.symm
-    rw [lwk1_let1, let1_seq, cfg_let1, let1_seq]
+    rw [let1_seq, vwk1_cfg]
+    simp only [vwk1_vwk2]
+    rw [Ir, <-cfg_let1]
     congr
-    apply Eq.trans (Ir g.vwk1 h.vwk1).symm
-    simp only [vwk1_cfg]
-    congr
-    funext i
-    cases i using Fin.elim1
-    simp [vwk1_vwk2]
+    sorry
   | let2 a r Ir =>
+    simp only [let2_seq, vwk1_cfg, vwk1_vwk2]
+    rw [Ir, <-cfg_let2]
+    congr
+    sorry
+  | case a l r Il Ir =>
+    simp only [case_seq, vwk1_cfg, vwk1_vwk2, Il, Ir]
+    rw [<-cfg_case]
+    congr
     sorry
-  | case a l r Il Ir => sorry
-  | cfg R β G Iβ IG => sorry
+  | cfg β dβ dG Iβ IG =>
+    conv =>
+      rhs
+      simp only [lwk_cfg, seq, lsubst_cfg, ushf_eq_cast, cast_cfg]
+      rw [cfg_cfg_eq_cfg']
+    sorry
+
+theorem Eqv.seq_cont {A B C : Ty α} {Γ : Ctx α ε} {L : LCtx α}
+  (f : Eqv φ (⟨A, ⊥⟩::Γ) (B::L)) (g : Eqv φ (⟨B, ⊥⟩::Γ) (C::D::L))
+  (h : Eqv φ (⟨C, ⊥⟩::Γ) (C::D::L))
+  : f ;; cfg [C] g (Fin.elim1 h.vwk1) = cfg [C] (f.lwk1 ;; g) (Fin.elim1 h.vwk1)
+  := by
+  have hc := Eqv.seq_cfg (R := [C]) f g (Fin.elim1 h)
+  convert hc
+  · rename Fin 1 => i; cases i using Fin.elim1; rfl
+  · induction f using Quotient.inductionOn
+    induction g using Quotient.inductionOn
+    induction h using Quotient.inductionOn
+    apply Eqv.eq_of_reg_eq
+    rfl
+  · rename Fin 1 => i; cases i using Fin.elim1; rfl
 
 theorem Eqv.ret_var_zero_eq_nil_vwk1 {A : Ty α} {Γ : Ctx α ε} {L : LCtx α}
   : ret (var 0 (by simp)) = (nil (φ := φ) (ty := A) (rest := Γ) (targets := L)).vwk1 (inserted := X)
diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Region/Eqv.lean b/DeBruijnSSA/BinSyntax/Rewrite/Region/Eqv.lean
index 946dbc9..cefff9e 100644
--- a/DeBruijnSSA/BinSyntax/Rewrite/Region/Eqv.lean
+++ b/DeBruijnSSA/BinSyntax/Rewrite/Region/Eqv.lean
@@ -146,6 +146,49 @@ theorem Eqv.cfg_eq_quot {R : LCtx α}
   : cfg R β G = ⟦InS.cfg R β' G'⟧ := by
   rw [hβ, funext hG, cfg_quot]
 
+theorem Eqv.cast_br {Γ : Ctx α ε} {L : LCtx α} {ℓ : ℕ} {A : Ty α}
+  (hΓ : Γ = Γ') (hL : L = L')
+  (a : Term.Eqv φ Γ ⟨A, ⊥⟩) (hℓ : L.Trg ℓ A)
+  : (br ℓ a hℓ).cast hΓ hL = br ℓ (a.cast hΓ rfl) (hL ▸ hℓ) := by
+  induction a using Quotient.inductionOn
+  rfl
+
+theorem Eqv.cast_let1 {Γ : Ctx α ε} {L : LCtx α} {A : Ty α} {e : ε}
+  (hΓ : Γ = Γ') (hL : L = L')
+  (a : Term.Eqv φ Γ ⟨A, e⟩) (r : Eqv φ (⟨A, ⊥⟩::Γ) L)
+  : (let1 a r).cast hΓ hL = let1 (a.cast hΓ rfl) (r.cast (Γ' := (A, ⊥)::Γ') (by rw [hΓ]) hL) := by
+  induction a using Quotient.inductionOn
+  induction r using Quotient.inductionOn
+  rfl
+
+theorem Eqv.cast_let2 {Γ : Ctx α ε} {L : LCtx α} {A B : Ty α} {e : ε}
+  (hΓ : Γ = Γ') (hL : L = L')
+  (a : Term.Eqv φ Γ ⟨Ty.prod A B, e⟩) (r : Eqv φ (⟨B, ⊥⟩::⟨A, ⊥⟩::Γ) L)
+  : (let2 a r).cast hΓ hL = let2 (a.cast hΓ rfl) (r.cast (Γ' := (B, ⊥)::(A, ⊥)::Γ') (by rw [hΓ]) hL)
+  := by
+  induction a using Quotient.inductionOn
+  induction r using Quotient.inductionOn
+  rfl
+
+theorem Eqv.cast_case {Γ : Ctx α ε} {L : LCtx α} {A B : Ty α} {e : ε}
+  (hΓ : Γ = Γ') (hL : L = L')
+  (a : Term.Eqv φ Γ ⟨Ty.coprod A B, e⟩) (r : Eqv φ (⟨A, ⊥⟩::Γ) L) (s : Eqv φ (⟨B, ⊥⟩::Γ) L)
+  : (case a r s).cast hΓ hL = case (a.cast hΓ rfl) (r.cast (Γ' := (A, ⊥)::Γ') (by rw [hΓ]) hL)
+    (s.cast (Γ' := (B, ⊥)::Γ') (by rw [hΓ]) hL) := by
+  induction a using Quotient.inductionOn
+  induction r using Quotient.inductionOn
+  induction s using Quotient.inductionOn
+  rfl
+
+theorem Eqv.cast_cfg {Γ : Ctx α ε} {L : LCtx α} {R : LCtx α}
+  (hΓ : Γ = Γ') (hL : L = L')
+  (β : Eqv φ Γ (R ++ L)) (G : ∀i, Eqv φ (⟨R.get i, ⊥⟩::Γ) (R ++ L))
+  : (cfg R β G).cast hΓ hL =
+    cfg R (β.cast hΓ (by rw [hL]))
+    (λi => (G i).cast (Γ' := (R.get i, ⊥)::Γ') (by rw [hΓ]) (by rw [hL])) := by
+  induction β using Quotient.inductionOn
+  sorry
+
 def Eqv.induction
   {motive : (Γ : Ctx α ε) → (L : LCtx α) → Eqv φ Γ L → Prop}
   (br : ∀{Γ L A} (ℓ) (a : Term.Eqv φ Γ ⟨A, ⊥⟩) (hℓ : L.Trg ℓ A), motive Γ L (Eqv.br ℓ a hℓ))
@@ -173,6 +216,90 @@ def Eqv.induction
       rw [cfg_quot] at res
       exact res
 
+def Eqv.shf {Γ : Ctx α ε} {L : LCtx α} {R : LCtx α} {Y : Ty α}
+  (d : Eqv φ Γ (R ++ (Y::L))) : Eqv φ Γ ((LCtx.shf_first R Y L)::(LCtx.shf_rest R Y L))
+  := Quotient.liftOn d (λd => ⟦d.shf⟧)
+    (λ_ _ h => Quotient.sound sorry)
+
+@[simp]
+theorem Eqv.shf_quot {Γ : Ctx α ε} {L : LCtx α} {R : LCtx α} {Y : Ty α}
+  (d : InS φ Γ (R ++ (Y::L))) : shf ⟦d⟧ = ⟦d.shf⟧ := rfl
+
+theorem Eqv.shf_eq_cast {Γ : Ctx α ε} {L : LCtx α} {R : LCtx α} {Y : Ty α}
+  (d : Eqv φ Γ (R ++ (Y::L))) : d.shf = d.cast rfl LCtx.shf_eq := rfl
+
+@[simp]
+theorem Eqv.shf_br {Γ : Ctx α ε} {L : LCtx α} {ℓ : ℕ} {A : Ty α}
+  (a : Term.Eqv φ Γ ⟨A, ⊥⟩) (hℓ : LCtx.Trg (R ++ (Y :: L)) ℓ A)
+  : (br ℓ a hℓ).shf = br ℓ a (LCtx.shf_eq ▸ hℓ) := by
+  induction a using Quotient.inductionOn
+  rfl
+
+@[simp]
+theorem Eqv.shf_let1 {Γ : Ctx α ε} {L : LCtx α} {A : Ty α} {e : ε}
+  (a : Term.Eqv φ Γ ⟨A, e⟩) (r : Eqv φ (⟨A, ⊥⟩::Γ) (R ++ (Y::L)))
+  : (let1 a r).shf = let1 a (r.shf) := by
+  induction a using Quotient.inductionOn
+  induction r using Quotient.inductionOn
+  rfl
+
+@[simp]
+theorem Eqv.shf_let2 {Γ : Ctx α ε} {L : LCtx α} {A B : Ty α} {e : ε}
+  (a : Term.Eqv φ Γ ⟨Ty.prod A B, e⟩) (r : Eqv φ (⟨B, ⊥⟩::⟨A, ⊥⟩::Γ) (R ++ (Y::L)))
+  : (let2 a r).shf = let2 a (r.shf) := by
+  induction a using Quotient.inductionOn
+  induction r using Quotient.inductionOn
+  rfl
+
+@[simp]
+theorem Eqv.shf_case {Γ : Ctx α ε} {L : LCtx α} {A B : Ty α} {e : ε}
+  (a : Term.Eqv φ Γ ⟨Ty.coprod A B, e⟩)
+  (r : Eqv φ (⟨A, ⊥⟩::Γ) (R ++ (Y::L))) (s : Eqv φ (⟨B, ⊥⟩::Γ) (R ++ (Y::L)))
+  : (case a r s).shf = case a (r.shf) (s.shf) := by
+  induction a using Quotient.inductionOn
+  induction r using Quotient.inductionOn
+  induction s using Quotient.inductionOn
+  rfl
+
+-- theorem Eqv.shf_cfg {Γ : Ctx α ε} {L : LCtx α} {R : LCtx α}
+--   (dβ : Eqv φ Γ (R' ++ (R ++ (Y::L)))) (dG : ∀i, Eqv φ (⟨R'.get i, ⊥⟩::Γ) (R' ++ (R ++ (Y::L))))
+--   : (cfg R' dβ dG).shf = cfg R' (dβ.shf) (λi => (dG i).shf) := by
+--   induction dβ using Quotient.inductionOn
+--   simp [Eqv.cfg, Eqv.cfg_inner, Quotient.finChoice_eq]
+
+def Eqv.ushf {Γ : Ctx α ε} {L : LCtx α} {R : LCtx α} {Y : Ty α}
+  (d : Eqv φ Γ ((LCtx.shf_first R Y L)::(LCtx.shf_rest R Y L))) : Eqv φ Γ (R ++ (Y::L))
+  := Quotient.liftOn d (λd => ⟦d.ushf⟧)
+    (λ_ _ h => Quotient.sound sorry)
+
+@[simp]
+theorem Eqv.ushf_quot {Γ : Ctx α ε} {L : LCtx α} {R : LCtx α} {Y : Ty α}
+  (d : InS φ Γ ((LCtx.shf_first R Y L)::(LCtx.shf_rest R Y L))) : ushf ⟦d⟧ = ⟦d.ushf⟧ := rfl
+
+theorem Eqv.ushf_eq_cast {Γ : Ctx α ε} {L : LCtx α} {R : LCtx α} {Y : Ty α}
+  (d : Eqv φ Γ ((LCtx.shf_first R Y L)::(LCtx.shf_rest R Y L)))
+  : d.ushf = d.cast rfl LCtx.shf_eq.symm := rfl
+
+@[simp]
+theorem Eqv.shf_ushf {Γ : Ctx α ε} {L : LCtx α} {R : LCtx α} {Y : Ty α}
+  (d : Eqv φ Γ (R ++ (Y::L))) : d.shf.ushf = d
+  := by induction d using Quotient.inductionOn; rfl
+
+@[simp]
+theorem Eqv.ushf_shf {Γ : Ctx α ε} {L : LCtx α} {R : LCtx α} {Y : Ty α}
+  (d : Eqv φ Γ ((LCtx.shf_first R Y L)::(LCtx.shf_rest R Y L))) : d.ushf.shf = d
+  := by induction d using Quotient.inductionOn; rfl
+
+@[simp]
+theorem Eqv.shf_inj {Γ : Ctx α ε} {L : LCtx α} {R : LCtx α} {Y : Ty α}
+  {d₁ d₂ : Eqv φ Γ (R ++ (Y::L))} :
+   d₁.shf = d₂.shf ↔ d₁ = d₂ := ⟨λh => by convert congrArg ushf h <;> simp, λh => congrArg _ h⟩
+
+@[simp]
+theorem Eqv.ushf_inj {Γ : Ctx α ε} {L : LCtx α} {R : LCtx α} {Y : Ty α}
+  {d₁ d₂ : Eqv φ Γ ((LCtx.shf_first R Y L)::(LCtx.shf_rest R Y L))} :
+   d₁.ushf = d₂.ushf ↔ d₁ = d₂ := by rw [<-shf_inj]; simp
+
 theorem Eqv.arrow_induction
   {motive : (X : Ty α) → (Γ : Ctx α ε) → (Y : Ty α) → (L : LCtx α)
     → Eqv φ ((X, ⊥)::Γ) (Y::L) → Prop}
@@ -189,8 +316,8 @@ theorem Eqv.arrow_induction
   (cfg : ∀{X Γ Y L} (R)
     (dβ : Eqv φ ((X, ⊥)::Γ) (R ++ (Y :: L)))
     (dG : ∀i : Fin R.length, Eqv φ (⟨R.get i, ⊥⟩::⟨X, ⊥⟩::Γ) (R ++ (Y :: L))),
-    motive X Γ _ _ (dβ.cast rfl output_reshuffle_helper)
-    → (∀i, motive _ _ _ _ ((dG i).cast rfl output_reshuffle_helper))
+    motive X Γ _ _ dβ.shf
+    → (∀i, motive _ _ _ _ (dG i).shf)
     → motive _ Γ _ L (Eqv.cfg R dβ dG))
   {X Γ Y L} (r : Eqv φ ((X, ⊥)::Γ) (Y::L)) : motive _ _ _ _ r := by
   induction r using Quotient.inductionOn with
@@ -301,7 +428,41 @@ theorem InS.lwk_q {Γ : Ctx α ε} {L K : LCtx α} {ρ : L.InS K} {r : InS φ Γ
 theorem Eqv.lwk_quot {Γ : Ctx α ε} {L K : LCtx α} {ρ : L.InS K} {r : InS φ Γ L}
    : Eqv.lwk ρ ⟦r⟧ = ⟦r.lwk ρ⟧ := rfl
 
--- TODO: lwk lemmas
+@[simp]
+theorem Eqv.lwk_br {Γ : Ctx α ε} {L K : LCtx α} {ρ : L.InS K}
+  {ℓ} {a : Term.Eqv φ Γ ⟨A, ⊥⟩} {hℓ : L.Trg ℓ A}
+  : Eqv.lwk ρ (Eqv.br ℓ a hℓ) = Eqv.br (ρ.val ℓ) a (hℓ.wk ρ.prop) := by
+  induction a using Quotient.inductionOn
+  rfl
+
+@[simp]
+theorem Eqv.lwk_let1 {Γ : Ctx α ε} {L K : LCtx α} {ρ : L.InS K}
+  {a : Term.Eqv φ Γ ⟨A, e⟩} {r : Eqv φ (⟨A, ⊥⟩::Γ) L}
+  : (let1 a r).lwk ρ = let1 a (r.lwk ρ) := by
+  induction a using Quotient.inductionOn; induction r using Quotient.inductionOn; rfl
+
+@[simp]
+theorem Eqv.lwk_let2 {Γ : Ctx α ε} {L K : LCtx α} {ρ : L.InS K}
+  {a : Term.Eqv φ Γ ⟨Ty.prod A B, e⟩} {r : Eqv φ (⟨B, ⊥⟩::⟨A, ⊥⟩::Γ) L}
+  : (let2 a r).lwk ρ = let2 a (r.lwk ρ) := by
+  induction a using Quotient.inductionOn; induction r using Quotient.inductionOn; rfl
+
+@[simp]
+theorem Eqv.lwk_case {Γ : Ctx α ε} {L K : LCtx α} {ρ : L.InS K}
+  {e : Term.Eqv φ Γ ⟨Ty.coprod A B, e⟩}
+  {r : Eqv φ (⟨A, ⊥⟩::Γ) L} {s : Eqv φ (⟨B, ⊥⟩::Γ) L}
+  : (case e r s).lwk ρ = case e (r.lwk ρ) (s.lwk ρ) := by
+  induction e using Quotient.inductionOn
+  induction r using Quotient.inductionOn
+  induction s using Quotient.inductionOn
+  rfl
+
+@[simp]
+theorem Eqv.lwk_cfg {Γ : Ctx α ε} {L K : LCtx α} {ρ : L.InS K}
+  {R : LCtx α} {β : Eqv φ Γ (R ++ L)} {G : ∀i, Eqv φ (⟨R.get i, ⊥⟩::Γ) (R ++ L)}
+  : (cfg R β G).lwk ρ = cfg R (β.lwk (ρ.liftn_append _)) (λi => (G i).lwk (ρ.liftn_append _)) := by
+  induction β using Quotient.inductionOn
+  sorry
 
 theorem InS.vsubst_q {Γ Δ : Ctx α ε} {L : LCtx α} {σ : Term.Subst.InS φ Γ Δ} {r : InS φ Δ L}
    : (r.q).vsubst σ.q = (r.vsubst σ).q := rfl
@@ -868,18 +1029,29 @@ theorem Eqv.cfg_case {Γ : Ctx α ε} {L : LCtx α}
     apply Eq.symm
     apply Quotient.forall_of_finChoice_eq hG
 
--- theorem Eqv.cfg_eqv_cfg' {Γ : Ctx α ε} {L : LCtx α}
---   (R S : LCtx α) (β : Eqv φ Γ (R ++ (S ++ L)))
---   (G : (i : Fin R.length) → Eqv φ (⟨R.get i, ⊥⟩::Γ) (R ++ (S ++ L)))
---   (G' : (i : Fin S.length) → Eqv φ (⟨S.get i, ⊥⟩::Γ) (S ++ L))
---     : (β.cfg R G).cfg S G'
---     = (β.cast rfl (by rw [List.append_assoc])).cfg'
---       (R.length + S.length) (R ++ S) (by rw [List.length_append])
---       (Fin.addCases (λi => (G i).cast (by sorry) (by rw [List.append_assoc]))
---                     (λi => ((G' i).lwk (· + R.length) sorry).cast sorry
---                       (by rw [List.append_assoc]))
---       )
---   := sorry
+theorem Eqv.cfg_cfg_eq_cfg' {Γ : Ctx α ε} {L : LCtx α}
+  (R S : LCtx α) (β : Eqv φ Γ (R ++ (S ++ L)))
+  (G : (i : Fin R.length) → Eqv φ (⟨R.get i, ⊥⟩::Γ) (R ++ (S ++ L)))
+  (G' : (i : Fin S.length) → Eqv φ (⟨S.get i, ⊥⟩::Γ) (S ++ L))
+    : (β.cfg R G).cfg S G'
+    = (β.cast rfl (by rw [List.append_assoc])).cfg'
+      (R.length + S.length) (R ++ S) (by rw [List.length_append])
+      (Fin.addCases
+        (λi => (G i).cast (by
+          simp only [List.get_eq_getElem, Fin.cast, Fin.coe_castAdd]
+          rw [List.getElem_append]
+          -- TODO: put in discretion
+          ) (by rw [List.append_assoc]))
+        (λi => ((G' i).lwk (LCtx.InS.add_left_append (S ++ L) R)).cast (by
+          simp only [List.get_eq_getElem, Fin.cast, Fin.coe_natAdd]
+          rw [List.getElem_append_right]
+          simp
+          omega
+          omega
+          -- TODO: put in discretion
+        )
+          (by rw [List.append_assoc])))
+  := sorry
 
 theorem Eqv.cfg_zero {Γ : Ctx α ε} {L : LCtx α}
   (β : Eqv φ Γ L)
diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Region/LSubst.lean b/DeBruijnSSA/BinSyntax/Rewrite/Region/LSubst.lean
index 346549f..7de6b33 100644
--- a/DeBruijnSSA/BinSyntax/Rewrite/Region/LSubst.lean
+++ b/DeBruijnSSA/BinSyntax/Rewrite/Region/LSubst.lean
@@ -95,7 +95,20 @@ theorem Eqv.lsubst_case {Γ : Ctx α ε} {L K : LCtx α} {σ : Subst.Eqv φ Γ L
   induction σ using Quotient.inductionOn
   rfl
 
--- TODO: lsubst_cfg
+def Subst.Eqv.liftn_append {Γ : Ctx α ε} {L K : LCtx α} (J) (σ : Subst.Eqv φ Γ L K)
+  : Subst.Eqv φ Γ (J ++ L) (J ++ K)
+  := Quotient.liftOn σ
+    (λσ => ⟦σ.liftn_append J⟧)
+    sorry
+
+@[simp]
+theorem Eqv.lsubst_cfg {Γ : Ctx α ε} {L : LCtx α}
+  {R : LCtx α} {β : Eqv φ Γ (R ++ L)} {G : ∀i, Eqv φ (⟨R.get i, ⊥⟩::Γ) (R ++ L)}
+  {σ : Subst.Eqv φ Γ L K}
+  : (cfg R β G).lsubst σ
+  = cfg R (β.lsubst (σ.liftn_append _)) (λi => (G i).lsubst (σ.liftn_append _).vlift) := by
+  induction β using Quotient.inductionOn
+  sorry
 
 def Subst.Eqv.vsubst {Γ Δ : Ctx α ε} {L K : LCtx α}
   (ρ : Term.Subst.Eqv φ Γ Δ) (σ : Subst.Eqv φ Δ L K) : Subst.Eqv φ Γ L K
diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Region/Setoid.lean b/DeBruijnSSA/BinSyntax/Rewrite/Region/Setoid.lean
index 2568a35..0165b94 100644
--- a/DeBruijnSSA/BinSyntax/Rewrite/Region/Setoid.lean
+++ b/DeBruijnSSA/BinSyntax/Rewrite/Region/Setoid.lean
@@ -337,8 +337,11 @@ theorem InS.cfg_cfg_eqv_cfg' {Γ : Ctx α ε} {L : LCtx α}
           ) (by rw [List.append_assoc]))
         (λi => ((G' i).lwk (LCtx.InS.add_left_append (S ++ L) R)).cast (by
           simp only [List.get_eq_getElem, Fin.cast, Fin.coe_natAdd]
+          rw [List.getElem_append_right]
+          simp
+          omega
+          omega
           -- TODO: put in discretion
-          sorry
         )
           (by rw [List.append_assoc])))
   := Uniform.rel $
diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Term/Eqv.lean b/DeBruijnSSA/BinSyntax/Rewrite/Term/Eqv.lean
index d3096f4..3662d93 100644
--- a/DeBruijnSSA/BinSyntax/Rewrite/Term/Eqv.lean
+++ b/DeBruijnSSA/BinSyntax/Rewrite/Term/Eqv.lean
@@ -24,6 +24,12 @@ theorem Eqv.sound {a a' : InS φ Γ V} (h : a ≈ a') : InS.q a = InS.q a' := Qu
 
 theorem Eqv.eq {a a' : InS φ Γ V} : a.q = a'.q ↔ a ≈ a' := Quotient.eq
 
+def Eqv.cast
+  (a : Eqv φ Γ V) (hΓ : Γ = Γ') (hV : V = V') : Eqv φ Γ' V'
+  := Quotient.liftOn a
+    (λa => ⟦a.cast hΓ hV⟧)
+    (λa a' h => Quotient.sound (by cases hΓ; cases hV; exact h))
+
 theorem Eqv.eq_of_term_eq {a a' : InS φ Γ V} (h : (a : Term φ) = (a' : Term φ))
   : a.q = a'.q := congrArg _ (InS.ext h)
 
diff --git a/DeBruijnSSA/BinSyntax/Typing/LCtx.lean b/DeBruijnSSA/BinSyntax/Typing/LCtx.lean
index 1c217d4..cb88c2d 100644
--- a/DeBruijnSSA/BinSyntax/Typing/LCtx.lean
+++ b/DeBruijnSSA/BinSyntax/Typing/LCtx.lean
@@ -99,6 +99,9 @@ theorem Wkn.liftn_append {L K : LCtx α} {ρ : ℕ → ℕ} (R : LCtx α) (h : L
   rw [<-Wkn_iff]
   exact h
 
+def InS.liftn_append {L K : LCtx α} (R : LCtx α) : InS L K → InS (R ++ L) (R ++ K)
+  := λρ => ⟨Nat.liftnWk R.length ρ, ρ.2.liftn_append R⟩
+
 theorem Wkn.comp {L K J : LCtx α} {ρ σ}
   : K.Wkn J ρ → L.Wkn K σ → L.Wkn J (ρ ∘ σ)
   := by
@@ -185,3 +188,42 @@ theorem Trg.rec_to_wkn_id {L R : LCtx α} {ℓ} {A : Ty α} (h : Trg (R ++ L) 
     have h' := h.getElem;
     rw [List.getElem_append_left] at h';
     exact h', le_refl _⟩
+
+def shf_first (R : LCtx α) (Y : Ty α) (L : LCtx α) : Ty α
+  := (R ++ (Y::L))[0]
+
+def shf_rest (R : LCtx α) (Y : Ty α) (L : LCtx α) : LCtx α
+  := (R ++ (Y::L)).drop 1
+
+theorem shf_eq {R : LCtx α} {Y : Ty α} {L : LCtx α}
+  : (R ++ (Y::L)) = (shf_first R Y L)::(shf_rest R Y L)
+  := by cases R <;> rfl
+
+@[simp]
+theorem length_shf_rest {R : LCtx α} {Y : Ty α} {L : LCtx α}
+  : (shf_rest R Y L).length = R.length + L.length
+  := by simp [shf_rest, drop, List.length_drop]
+
+@[simp]
+theorem getElem_shf_rest_add {R : LCtx α} {Y : Ty α} {L : LCtx α} {n}
+  {hn : n + R.length < (shf_rest R Y L).length}
+  : (shf_rest R Y L)[n + R.length] = L[n]'(by simp at hn; omega)
+  := by cases R with
+  | nil => rfl
+  | cons X R =>
+    simp only [shf_rest, drop, List.cons_append, List.drop_succ_cons, List.drop_zero,
+      List.length_cons, Nat.add_comm R.length 1, <-Nat.add_assoc]
+    rw [List.getElem_append_right]
+    simp only [Nat.add_sub_cancel]
+    simp
+    omega
+    simp at hn
+    simp only [add_tsub_cancel_right, List.length_cons, add_lt_add_iff_right]
+    omega
+
+theorem Wkn.shf {R : LCtx α} {Y : Ty α} {L : LCtx α}
+  : LCtx.Wkn L (shf_rest R Y L) (· + R.length)
+  := λi hi => ⟨by simp only [length_shf_rest]; omega, by simp⟩
+
+def InS.shf {R : LCtx α} {Y : Ty α} {L : LCtx α} : L.InS (shf_rest R Y L)
+  := ⟨(· + R.length), Wkn.shf⟩
diff --git a/DeBruijnSSA/BinSyntax/Typing/Region/Basic.lean b/DeBruijnSSA/BinSyntax/Typing/Region/Basic.lean
index f03df04..b8621aa 100644
--- a/DeBruijnSSA/BinSyntax/Typing/Region/Basic.lean
+++ b/DeBruijnSSA/BinSyntax/Typing/Region/Basic.lean
@@ -237,23 +237,13 @@ theorem InS.induction
     simp only [Fin.cast_eq_self] at *
     exact cfg R ⟨_, dβ⟩ (λi => ⟨_, dG i⟩) Iβ IG
 
-def output_first (R : LCtx α) (Y : Ty α) (L : LCtx α) : Ty α
-  := (R ++ (Y::L))[0]
-
-def output_rest (R : LCtx α) (Y : Ty α) (L : LCtx α) : LCtx α
-  := (R ++ (Y::L)).drop 1
-
-theorem output_reshuffle_helper {R : LCtx α} {Y : Ty α} {L : LCtx α}
-  : (R ++ (Y::L)) = (output_first R Y L)::(output_rest R Y L)
-  := by cases R <;> rfl
-
 def InS.shf {Γ : Ctx α ε} {L : LCtx α} {R : LCtx α} {Y : Ty α}
-  (d : InS φ Γ (R ++ (Y::L))) : InS φ Γ ((output_first R Y L)::(output_rest R Y L))
-  := d.cast rfl output_reshuffle_helper
+  (d : InS φ Γ (R ++ (Y::L))) : InS φ Γ ((LCtx.shf_first R Y L)::(LCtx.shf_rest R Y L))
+  := d.cast rfl LCtx.shf_eq
 
 def InS.ushf {Γ : Ctx α ε} {L : LCtx α} {R : LCtx α} {Y : Ty α}
-  (d : InS φ Γ ((output_first R Y L)::(output_rest R Y L))) : InS φ Γ (R ++ (Y::L))
-  := d.cast rfl output_reshuffle_helper.symm
+  (d : InS φ Γ ((LCtx.shf_first R Y L)::(LCtx.shf_rest R Y L))) : InS φ Γ (R ++ (Y::L))
+  := d.cast rfl LCtx.shf_eq.symm
 
 @[simp]
 theorem InS.shf_ushf {Γ : Ctx α ε} {L : LCtx α} {R : LCtx α} {Y : Ty α}
@@ -262,7 +252,7 @@ theorem InS.shf_ushf {Γ : Ctx α ε} {L : LCtx α} {R : LCtx α} {Y : Ty α}
 
 @[simp]
 theorem InS.ushf_shf {Γ : Ctx α ε} {L : LCtx α} {R : LCtx α} {Y : Ty α}
-  (d : InS φ Γ ((output_first R Y L)::(output_rest R Y L))) : d.ushf.shf = d
+  (d : InS φ Γ ((LCtx.shf_first R Y L)::(LCtx.shf_rest R Y L))) : d.ushf.shf = d
   := by cases d; rfl
 
 @[simp]
@@ -272,7 +262,8 @@ theorem InS.coe_shf {Γ : Ctx α ε} {L : LCtx α} {R : LCtx α} {Y : Ty α}
 
 @[simp]
 theorem InS.coe_ushf {Γ : Ctx α ε} {L : LCtx α} {R : LCtx α} {Y : Ty α}
-  (d : InS φ Γ ((output_first R Y L)::(output_rest R Y L))) : (d.ushf : Region φ) = (d : Region φ)
+  (d : InS φ Γ ((LCtx.shf_first R Y L)::(LCtx.shf_rest R Y L)))
+  : (d.ushf : Region φ) = (d : Region φ)
   := rfl
 
 @[simp]
@@ -282,7 +273,7 @@ theorem InS.shf_inj {Γ : Ctx α ε} {L : LCtx α} {R : LCtx α} {Y : Ty α}
 
 @[simp]
 theorem InS.ushf_inj {Γ : Ctx α ε} {L : LCtx α} {R : LCtx α} {Y : Ty α}
-  {r r' : InS φ Γ ((output_first R Y L)::(output_rest R Y L))} : r.ushf = r'.ushf ↔ r = r'
+  {r r' : InS φ Γ ((LCtx.shf_first R Y L)::(LCtx.shf_rest R Y L))} : r.ushf = r'.ushf ↔ r = r'
   := cast_inj
 
 theorem InS.arrow_induction
@@ -336,13 +327,13 @@ theorem InS.arrow_induction
       cases hR
       simp only [Fin.cast_eq_self] at *
       apply cfg R ⟨_, dβ⟩ (λi => ⟨_, dG i⟩)
-      exact Iβ (output_reshuffle_helper ▸ dβ) rfl rfl
-        output_reshuffle_helper.symm
-        output_reshuffle_helper.symm
+      exact Iβ (LCtx.shf_eq ▸ dβ) rfl rfl
+        LCtx.shf_eq.symm
+        LCtx.shf_eq.symm
       intro i
-      apply IG i (output_reshuffle_helper ▸ dG i) rfl rfl
-        output_reshuffle_helper.symm
-        output_reshuffle_helper.symm
+      apply IG i (LCtx.shf_eq ▸ dG i) rfl rfl
+        LCtx.shf_eq.symm
+        LCtx.shf_eq.symm
 
 def InD (φ) [EffInstSet φ (Ty α) ε] (Γ : Ctx α ε) (L : LCtx α) : Type _
   := Σr : Region φ, r.WfD Γ L
diff --git a/DeBruijnSSA/BinSyntax/Typing/Region/LSubst.lean b/DeBruijnSSA/BinSyntax/Typing/Region/LSubst.lean
index 1d662c6..1899e26 100644
--- a/DeBruijnSSA/BinSyntax/Typing/Region/LSubst.lean
+++ b/DeBruijnSSA/BinSyntax/Typing/Region/LSubst.lean
@@ -81,6 +81,10 @@ theorem Region.Subst.Wf.liftn_append (J : LCtx α) (hσ : σ.Wf Γ L K)
   | [] => by rw [List.nil_append, List.nil_append, List.length_nil, liftn_zero]; exact hσ
   | A::J => by rw [List.length_cons, liftn_succ]; exact (hσ.liftn_append J).slift
 
+def Region.Subst.InS.liftn_append (J : LCtx α) (σ : Region.Subst.InS φ Γ L K)
+  : Region.Subst.InS φ Γ (J ++ L) (J ++ K)
+  := ⟨σ.val.liftn J.length, σ.prop.liftn_append J⟩
+
 def Region.Subst.WfD.liftn_append' {J : LCtx α} (hn : n = J.length) (hσ : σ.WfD Γ L K)
   : (σ.liftn n).WfD Γ (J ++ L) (J ++ K)
   := hn ▸ hσ.liftn_append J
diff --git a/DeBruijnSSA/BinSyntax/Typing/Term/Basic.lean b/DeBruijnSSA/BinSyntax/Typing/Term/Basic.lean
index f1e80a1..7d2737b 100644
--- a/DeBruijnSSA/BinSyntax/Typing/Term/Basic.lean
+++ b/DeBruijnSSA/BinSyntax/Typing/Term/Basic.lean
@@ -147,6 +147,9 @@ theorem Term.InS.coe_unit {Γ : Ctx α ε} {e}
   : (Term.InS.unit (φ := φ) (Γ := Γ) e : Term φ) = Term.unit
   := rfl
 
+def Term.InS.cast {Γ : Ctx α ε} {V} (a : InS φ Γ V) (hΓ : Γ = Γ') (hV : V = V')
+  : InS φ Γ' V' := ⟨a, hΓ ▸ hV ▸ a.prop⟩
+
 theorem Term.InS.induction
   {motive : (Γ : Ctx α ε) → (V : Ty α × ε) → InS φ Γ V → Prop}
   (var : ∀{Γ V} (n) (hv : Γ.Var n V), motive Γ V (Term.InS.var n hv))
@@ -371,8 +374,6 @@ theorem Term.Wf.to_right {Γ : Ctx α ε} {a b : Term φ}
   (h : Wf Γ (Term.pair a b) ⟨Ty.prod A B, e⟩)
   : Wf Γ b ⟨B, e⟩ := by cases h with | pair _ hb => exact hb
 
-
-
 @[simp]
 theorem Term.Wf.var_iff {Γ : Ctx α ε} {n V} : Wf (φ := φ) Γ (Term.var n) V ↔ Γ.Var n V
   := ⟨λ| Wf.var dv => dv, λdv => Wf.var dv⟩