Began gloop based structured control-flow implementation

DeBruijnSSA/BinSyntax/Rewrite/Region/Compose.lean

@@ -1,6 +1,6 @@
 import DeBruijnSSA.BinSyntax.Rewrite.Region.Compose.Seq
 import DeBruijnSSA.BinSyntax.Rewrite.Region.Compose.Product
 import DeBruijnSSA.BinSyntax.Rewrite.Region.Compose.Sum
-import DeBruijnSSA.BinSyntax.Rewrite.Region.Compose.Structural
+import DeBruijnSSA.BinSyntax.Rewrite.Region.Structural
 import DeBruijnSSA.BinSyntax.Rewrite.Region.Compose.Elgot
 import DeBruijnSSA.BinSyntax.Rewrite.Region.Compose.Completeness

DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Completeness.lean

@@ -1,4 +1,4 @@
-import DeBruijnSSA.BinSyntax.Rewrite.Region.Compose.Structural
+import DeBruijnSSA.BinSyntax.Rewrite.Region.Structural
 import DeBruijnSSA.BinSyntax.Rewrite.Region.Compose.Functor
 import DeBruijnSSA.BinSyntax.Rewrite.Region.Compose.Elgot
 

DeBruijnSSA/BinSyntax/Rewrite/Region/Eqv.lean

@@ -410,6 +410,10 @@ def Eqv.lwk_id {Γ : Ctx α ε} {L K : LCtx α} (hρ : L.Wkn K id) (r : Eqv φ 
       simp only [InS.lwk_id_eq_lwk]
       exact Quotient.sound (InS.lwk_congr_right _ h))
 
+theorem Eqv.lwk_id_eq_lwk {Γ : Ctx α ε} {L K : LCtx α} {r : Eqv φ Γ L}
+  (hρ : L.Wkn K id) : Eqv.lwk_id hρ r = r.lwk ⟨id, hρ⟩ := by
+  induction r using Quotient.inductionOn; apply eq_of_reg_eq; simp
+
 def Eqv.vsubst {Γ Δ : Ctx α ε} {L : LCtx α} (σ : Term.Subst.Eqv φ Γ Δ) (r : Eqv φ Δ L)
   : Eqv φ Γ L := Quotient.liftOn₂ σ r
     (λσ r => InS.q (r.vsubst σ))

DeBruijnSSA/BinSyntax/Rewrite/Region/LSubst.lean

@@ -107,6 +107,10 @@ theorem Subst.InS.extend_in_congr {Γ : Ctx α ε} {L K R : LCtx α}
       exact InS.hext (by rw [List.getElem_append_left]; rfl) rfl (by simp)
     case _ => rfl
 
+theorem Subst.InS.extend_out_congr {Γ : Ctx α ε} {L K R : LCtx α}
+  {σ τ : Subst.InS φ Γ L K} (h : σ ≈ τ) : σ.extend_out (R := R) ≈ τ.extend_out
+  := λi => Region.InS.lwk_id_congr (K := K ++ R) LCtx.Wkn.id_right_append (h i)
+
 open Subst.InS
 
 theorem InS.lsubst_congr_subst {Γ : Ctx α ε} {L K : LCtx α} {σ τ : Subst.InS φ Γ L K}
@@ -218,6 +222,35 @@ def Subst.Eqv.extend_in {Γ : Ctx α ε} {L K R : LCtx α} (σ : Eqv φ Γ L (K
 theorem Subst.Eqv.extend_in_quot {Γ : Ctx α ε} {L K R : LCtx α} {σ : Subst.InS φ Γ L (K ++ R)}
   : extend_in ⟦σ⟧ = ⟦σ.extend_in⟧ := rfl
 
+def Subst.Eqv.extend_out {Γ : Ctx α ε} {L K R : LCtx α} (σ : Eqv φ Γ L K)
+  : Eqv φ Γ L (K ++ R) := Quotient.liftOn σ (λσ => ⟦σ.extend_out⟧)
+    (λ_ _ h => Quotient.sound <| Subst.InS.extend_out_congr h)
+
+@[simp]
+theorem Subst.Eqv.extend_out_quot {Γ : Ctx α ε} {L K R : LCtx α} {σ : Subst.InS φ Γ L K}
+  : extend_out (R := R) ⟦σ⟧ = ⟦σ.extend_out⟧ := rfl
+
+theorem Subst.Eqv.extend_in_extend_out {Γ : Ctx α ε} {L K R : LCtx α} (σ : Eqv φ Γ L K)
+  : σ.extend_out.extend_in = σ.extend (R := R) := by
+  induction σ using Quotient.inductionOn
+  rw [extend_out_quot, extend_in_quot, Subst.InS.extend_in_extend_out]; rfl
+
+theorem Subst.Eqv.vlift_extend_in {Γ : Ctx α ε} {L K : LCtx α} {σ : Subst.Eqv φ Γ L (K ++ R)}
+  : σ.extend_in.vlift (head := head) = σ.vlift.extend_in
+  := by induction σ using Quotient.inductionOn; simp [Subst.InS.vlift_extend_in]
+
+theorem Subst.Eqv.vlift_extend_out {Γ : Ctx α ε} {L K : LCtx α} {σ : Subst.Eqv φ Γ L K}
+  : σ.extend_out.vlift (head := head) = σ.vlift.extend_out (R := R)
+  := by induction σ using Quotient.inductionOn; rfl
+
+theorem Subst.Eqv.vlift_extend {Γ : Ctx α ε} {L K : LCtx α} {σ : Subst.Eqv φ Γ L K}
+  : σ.extend.vlift (head := head) = σ.vlift.extend (R := R)
+  := by rw [<-extend_in_extend_out, vlift_extend_in, vlift_extend_out, extend_in_extend_out]
+
+theorem Subst.Eqv.get_extend_out {Γ : Ctx α ε} {L K R : LCtx α} {σ : Subst.Eqv φ Γ L K}
+  {i : Fin L.length} : (extend_out (R := R) σ).get i = (σ.get i).lwk_id LCtx.Wkn.id_right_append
+  := by induction σ using Quotient.inductionOn; rfl
+
 @[simp]
 theorem InS.lsubst_q {Γ : Ctx α ε} {L K : LCtx α} {σ : Subst.InS φ Γ L K} {r : InS φ Γ L}
    : (r.q).lsubst ⟦σ⟧ = (r.lsubst σ).q := rfl
@@ -638,6 +671,11 @@ def Subst.Eqv.fromFCFG {Γ : Ctx α ε} {L K : LCtx α}
   := Quotient.liftOn (Quotient.finChoice G) (λG => ⟦Region.CFG.toSubst G⟧)
       (λ_ _ h => Quotient.sound <| λi => by simp [h i])
 
+theorem Subst.Eqv.fromFCFG_quot {Γ : Ctx α ε} {L K : LCtx α}
+  {G : ∀i : Fin L.length, Region.InS φ ((L.get i, ⊥)::Γ) K}
+  : fromFCFG (λi => ⟦G i⟧) = ⟦Region.CFG.toSubst G⟧ := by
+  simp [fromFCFG, Quotient.finChoice_eq_choice]
+
 def Subst.Eqv.fromFCFG_append {Γ : Ctx α ε} {L K R : LCtx α}
   (G : ∀i : Fin L.length, Region.Eqv φ ((L.get i, ⊥)::Γ) (K ++ R))
   : Subst.Eqv φ Γ (L ++ R) (K ++ R)
@@ -688,20 +726,49 @@ theorem Eqv.dinaturality {Γ : Ctx α ε} {R R' L : LCtx α}
     rw [Subst.Eqv.fromFCFG_append_quot]
     simp [Subst.InS.cfg]
 
+theorem Eqv.dinaturality_rec {Γ : Ctx α ε} {R R' L : LCtx α}
+  {σ : Subst.Eqv φ Γ R R'} {β : Eqv φ Γ (R ++ L)}
+  {G : (i : Fin R'.length) → Eqv φ (⟨R'.get i, ⊥⟩::Γ) (R ++ L)}
+  : cfg R' (β.lsubst σ.extend) (λi => (G i).lsubst σ.extend.vlift)
+  = cfg R β (λi => (σ.get i).lsubst (Subst.Eqv.fromFCFG G).vlift)
+  := by
+  rw [<-Subst.Eqv.extend_in_extend_out, dinaturality]
+  congr; funext i
+  rw [Subst.Eqv.get_extend_out, lwk_id_eq_lwk, <-Eqv.lsubst_toSubst, lsubst_lsubst]
+  congr; ext k
+  induction G using Eqv.choiceInduction
+  rw [Subst.Eqv.fromFCFG_append_quot, Subst.Eqv.fromFCFG_quot]
+  apply Eqv.eq_of_reg_eq
+  simp [Subst.fromFCFG, Subst.vlift, Region.vsubst0_var0_vwk1]
+
 theorem Eqv.dinaturality_from_one {Γ : Ctx α ε} {R L : LCtx α}
   {σ : Subst.Eqv φ Γ R (B::L)} {β : Eqv φ Γ (R ++ L)}
   {G : Eqv φ (⟨B, ⊥⟩::Γ) (R ++ L)}
   : cfg [B] (β.lsubst σ.extend_in) (Fin.elim1 $ G.lsubst σ.extend_in.vlift)
   = cfg R β (λi => (σ.get i).lsubst (Subst.Eqv.fromFCFG_append (L := [B]) (Fin.elim1 G)).vlift)
   := dinaturality (Γ := Γ) (R := R) (R' := [B]) (L := L) (σ := σ) (β := β) (G := Fin.elim1 G)
 
+theorem Eqv.dinaturality_from_one_rec {Γ : Ctx α ε} {R L : LCtx α}
+  {σ : Subst.Eqv φ Γ R [B]} {β : Eqv φ Γ (R ++ L)}
+  {G : Eqv φ (⟨B, ⊥⟩::Γ) (R ++ L)}
+  : cfg [B] (β.lsubst σ.extend) (Fin.elim1 $ G.lsubst σ.extend.vlift)
+  = cfg R β (λi => (σ.get i).lsubst (Subst.Eqv.fromFCFG (Fin.elim1 G)).vlift)
+  := dinaturality_rec (Γ := Γ) (R := R) (R' := [B]) (L := L) (σ := σ) (β := β) (G := Fin.elim1 G)
+
 theorem Eqv.dinaturality_to_one {Γ : Ctx α ε} {R' L : LCtx α}
   {σ : Subst.Eqv φ Γ [A] (R' ++ L)} {β : Eqv φ Γ (A::L)}
   {G : (i : Fin R'.length) → Eqv φ (⟨R'.get i, ⊥⟩::Γ) (A::L)}
   : cfg R' (β.lsubst σ.extend_in) (λi => (G i).lsubst σ.extend_in.vlift)
   = cfg [A] β (Fin.elim1 $ (σ.get _).lsubst (Subst.Eqv.fromFCFG_append G).vlift)
   := dinaturality (Γ := Γ) (R := [A]) (R' := R') (L := L) (σ := σ) (β := β) (G := G)
 
+theorem Eqv.dinaturality_to_one_rec {Γ : Ctx α ε} {R' L : LCtx α}
+  {σ : Subst.Eqv φ Γ [A] R'} {β : Eqv φ Γ (A::L)}
+  {G : (i : Fin R'.length) → Eqv φ (⟨R'.get i, ⊥⟩::Γ) (A::L)}
+  : cfg R' (β.lsubst σ.extend) (λi => (G i).lsubst σ.extend.vlift)
+  = cfg [A] β (Fin.elim1 $ (σ.get _).lsubst (Subst.Eqv.fromFCFG G).vlift)
+  := dinaturality_rec (Γ := Γ) (R := [A]) (R' := R') (L := L) (σ := σ) (β := β) (G := G)
+
 theorem Eqv.dinaturality_one {Γ : Ctx α ε} {L : LCtx α}
   {σ : Subst.Eqv φ Γ [A] ([B] ++ L)} {β : Eqv φ Γ (A::L)}
   {G : Eqv φ (⟨B, ⊥⟩::Γ) ([A] ++ L)}

DeBruijnSSA/BinSyntax/Rewrite/Region/Setoid.lean

@@ -141,6 +141,10 @@ theorem InS.lwk_congr {Γ : Ctx α ε} {L K : LCtx α} {r r' : InS φ Γ L}
   {ρ ρ' : L.InS K} (hρ : ρ ≈ ρ') (hr : r ≈ r') : r.lwk ρ ≈ r'.lwk ρ'
   := r.lwk_equiv hρ ▸ lwk_congr_right ρ' hr
 
+theorem InS.lwk_id_congr {Γ : Ctx α ε} {L K : LCtx α} {r r' : InS φ Γ L}
+  (h : L.Wkn K id) (hr : r ≈ r') : r.lwk_id h ≈ r'.lwk_id h
+  := by rw [lwk_id_eq_lwk, lwk_id_eq_lwk]; apply lwk_congr_right; assumption
+
 theorem InS.let1_beta {Γ : Ctx α ε} {L : LCtx α}
   (a : Term.InS φ Γ ⟨A, ⊥⟩)
   (r : InS φ (⟨A, ⊥⟩::Γ) L)

DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Structural.lean → DeBruijnSSA/BinSyntax/Rewrite/Region/Structural.lean

@@ -1,6 +1,6 @@
-import DeBruijnSSA.BinSyntax.Rewrite.Region.Compose.Structural.Sum
-import DeBruijnSSA.BinSyntax.Rewrite.Region.Compose.Structural.Product
-import DeBruijnSSA.BinSyntax.Rewrite.Term.Compose.Structural
+import DeBruijnSSA.BinSyntax.Rewrite.Region.Structural.Sum
+import DeBruijnSSA.BinSyntax.Rewrite.Region.Structural.Product
+import DeBruijnSSA.BinSyntax.Rewrite.Term.Structural
 
 namespace BinSyntax
 

DeBruijnSSA/BinSyntax/Rewrite/Region/Structural/Gloop.lean

@@ -0,0 +1,79 @@
+import DeBruijnSSA.BinSyntax.Rewrite.Region.LSubst
+
+namespace BinSyntax
+
+variable [Φ: EffInstSet φ (Ty α) ε] [PartialOrder α] [SemilatticeSup ε] [OrderBot ε]
+
+namespace Region
+
+def Eqv.gloop {Γ : Ctx α ε} {L : LCtx α}
+  (A : Ty α) (β : Eqv φ Γ (A::L)) (G : Eqv φ ((A, ⊥)::Γ) (A::L)) : Eqv φ Γ L
+  := Eqv.cfg [A] β (Fin.elim1 G)
+
+theorem Eqv.cfg_eq_gloop {Γ : Ctx α ε} {L : LCtx α} {A : Ty α} {β : Eqv φ Γ (A::L)} {G}
+  : Eqv.cfg [A] β G = β.gloop A (G (0 : Fin 1)) := rfl
+
+@[simp]
+theorem Eqv.vwk_gloop {Γ Δ : Ctx α ε} {L : LCtx α}
+  {A : Ty α} {β : Eqv φ Δ (A::L)} {G : Eqv φ ((A, ⊥)::Δ) (A::L)} {ρ : Γ.InS Δ}
+  : (β.gloop A G).vwk ρ = (β.vwk ρ).gloop A (G.vwk ρ.slift)
+  := by rw [gloop, vwk_cfg]; rfl
+
+@[simp]
+theorem Eqv.vsubst_gloop {Γ Δ : Ctx α ε} {L : LCtx α}
+  {A : Ty α} {β : Eqv φ Δ (A::L)} {G : Eqv φ ((A, ⊥)::Δ) (A::L)} {σ : Term.Subst.Eqv φ Γ Δ}
+  : (β.gloop A G).vsubst σ = (β.vsubst σ).gloop A (G.vsubst (σ.lift (le_refl _)))
+  := by rw [gloop, vsubst_cfg]; rfl
+
+@[simp]
+theorem Eqv.lwk_gloop {Γ : Ctx α ε} {L K : LCtx α}
+  {A : Ty α} {β : Eqv φ Γ (A::L)} {G : Eqv φ ((A, ⊥)::Γ) (A::L)} {ρ : L.InS K}
+  : (β.gloop A G).lwk ρ = (β.lwk ρ.slift).gloop A (G.lwk ρ.slift) := by
+  rw [gloop, lwk_cfg]
+  congr
+  · ext k; simp [Nat.liftnWk_one]
+  · ext i; cases i using Fin.elim1
+    simp only [Fin.elim1_zero]
+    congr; ext k; simp [Nat.liftnWk_one]
+
+@[simp]
+theorem Eqv.lsubst_gloop {Γ : Ctx α ε} {L K : LCtx α}
+  {A : Ty α} {β : Eqv φ Γ (A::L)} {G : Eqv φ ((A, ⊥)::Γ) (A::L)} {σ : Subst.Eqv φ Γ L K}
+  : (β.gloop A G).lsubst σ = (β.lsubst σ.slift).gloop A (G.lsubst σ.slift.vlift)
+  := by rw [gloop, lsubst_cfg, Subst.Eqv.liftn_append_singleton]; rfl
+
+theorem Eqv.dinaturality_from_gloop {Γ : Ctx α ε} {R L : LCtx α}
+  {σ : Subst.Eqv φ Γ R ([B] ++ L)} {β : Eqv φ Γ (R ++ L)}
+  {G : Eqv φ (⟨B, ⊥⟩::Γ) (R ++ L)}
+  : gloop B (β.lsubst σ.extend_in) (G.lsubst σ.extend_in.vlift)
+  = cfg R β (λi => (σ.get i).lsubst (Subst.Eqv.fromFCFG_append (L := [B]) (Fin.elim1 G)).vlift)
+  := dinaturality (Γ := Γ) (R := R) (R' := [B]) (L := L) (σ := σ) (β := β) (G := Fin.elim1 G)
+
+theorem Eqv.dinaturality_from_gloop_rec {Γ : Ctx α ε} {R L : LCtx α}
+  {σ : Subst.Eqv φ Γ R [B]} {β : Eqv φ Γ (R ++ L)}
+  {G : Eqv φ (⟨B, ⊥⟩::Γ) (R ++ L)}
+  : gloop B (β.lsubst σ.extend) (G.lsubst σ.extend.vlift)
+  = cfg R β (λi => (σ.get i).lsubst (Subst.Eqv.fromFCFG (Fin.elim1 G)).vlift)
+  := dinaturality_rec (Γ := Γ) (R := R) (R' := [B]) (L := L) (σ := σ) (β := β) (G := Fin.elim1 G)
+
+theorem Eqv.dinaturality_to_gloop {Γ : Ctx α ε} {R' L : LCtx α}
+  {σ : Subst.Eqv φ Γ [A] (R' ++ L)} {β : Eqv φ Γ (A::L)}
+  {G : (i : Fin R'.length) → Eqv φ (⟨R'.get i, ⊥⟩::Γ) ([A] ++ L)}
+  : cfg R' (β.lsubst σ.extend_in) (λi => (G i).lsubst σ.extend_in.vlift)
+  = gloop A β ((σ.get (0 : Fin 1)).lsubst (Subst.Eqv.fromFCFG_append G).vlift)
+  := dinaturality (Γ := Γ) (R := [A]) (R' := R') (L := L) (σ := σ) (β := β) (G := G)
+
+theorem Eqv.dinaturality_to_gloop_rec {Γ : Ctx α ε} {R' L : LCtx α}
+  {σ : Subst.Eqv φ Γ [A] R'} {β : Eqv φ Γ (A::L)}
+  {G : (i : Fin R'.length) → Eqv φ (⟨R'.get i, ⊥⟩::Γ) ([A] ++ L)}
+  : cfg R' (β.lsubst σ.extend) (λi => (G i).lsubst σ.extend.vlift)
+  = gloop A β ((σ.get (0 : Fin 1)).lsubst (Subst.Eqv.fromFCFG G).vlift)
+  := dinaturality_rec (Γ := Γ) (R := [A]) (R' := R') (L := L) (σ := σ) (β := β) (G := G)
+
+theorem Eqv.dinaturality_gloop {Γ : Ctx α ε} {L : LCtx α}
+  {σ : Subst.Eqv φ Γ [A] ([B] ++ L)} {β : Eqv φ Γ (A::L)}
+  {G : Eqv φ (⟨B, ⊥⟩::Γ) (A::L)}
+  : gloop B (β.lsubst σ.extend_in) (G.lsubst σ.extend_in.vlift)
+  = gloop A β ((σ.get (0 : Fin 1)).lsubst
+    (Subst.Eqv.fromFCFG_append (K := [A]) (Fin.elim1 G)).vlift)
+  := dinaturality (Γ := Γ) (R := [A]) (R' := [B]) (L := L) (σ := σ) (β := β) (G := Fin.elim1 G)

DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Structural/Product.lean → DeBruijnSSA/BinSyntax/Rewrite/Region/Structural/Product.lean

@@ -1,7 +1,7 @@
 import DeBruijnSSA.BinSyntax.Rewrite.Region.LSubst
 import DeBruijnSSA.BinSyntax.Rewrite.Region.Compose.Seq
 import DeBruijnSSA.BinSyntax.Rewrite.Region.Compose.Sum
-import DeBruijnSSA.BinSyntax.Rewrite.Term.Compose.Structural.Product
+import DeBruijnSSA.BinSyntax.Rewrite.Term.Structural.Product
 import DeBruijnSSA.BinSyntax.Typing.Region.Structural
 
 namespace BinSyntax

DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Structural/Sum.lean → DeBruijnSSA/BinSyntax/Rewrite/Region/Structural/Sum.lean

@@ -1,7 +1,8 @@
 import DeBruijnSSA.BinSyntax.Rewrite.Region.LSubst
 import DeBruijnSSA.BinSyntax.Rewrite.Region.Compose.Seq
 import DeBruijnSSA.BinSyntax.Rewrite.Region.Compose.Sum
-import DeBruijnSSA.BinSyntax.Rewrite.Term.Compose.Structural.Sum
+import DeBruijnSSA.BinSyntax.Rewrite.Region.Structural.Gloop
+import DeBruijnSSA.BinSyntax.Rewrite.Term.Structural.Sum
 import DeBruijnSSA.BinSyntax.Typing.Region.Structural
 
 namespace BinSyntax
@@ -51,6 +52,10 @@ theorem Subst.Eqv.unpack_def {Γ : Ctx α ε} {R : LCtx α}
   : Subst.Eqv.unpack (φ := φ) (Γ := Γ) (R := R) = ⟦InS.unpack (Γ := Γ) (R := R)⟧
   := by rw [unpack, Region.Eqv.unpack_def]; rfl
 
+theorem Subst.Eqv.unpack_zero {Γ : Ctx α ε} {R : LCtx α}
+  : (Subst.Eqv.unpack (φ := φ) (Γ := Γ) (R := R)).get (0 : Fin 1) = Region.Eqv.unpack
+  := by rw [unpack_def, Region.Eqv.unpack_def]; rfl
+
 @[simp]
 theorem Subst.Eqv.vlift_unpack {Γ : Ctx α ε} {R : LCtx α}
   : (Subst.Eqv.unpack (φ := φ) (Γ := Γ) (R := R)).vlift (head := head) = unpack := by
@@ -219,3 +224,21 @@ theorem Eqv.unpacked_out_inj {Γ : Ctx α ε} {R : LCtx α} {r s : Eqv φ Γ [R.
 
 theorem Eqv.packed_out_inj {Γ : Ctx α ε} {R : LCtx α} {r s : Eqv φ Γ R}
   : r.packed_out = s.packed_out ↔ r = s := ⟨λh => packed_out_injective h, λh => by simp [h]⟩
+
+theorem Eqv.cfg_unpack_rec {Γ : Ctx α ε} {R L : LCtx α}
+  {β : Eqv φ Γ (R.pack::L)} {G : (i : Fin R.length) → Eqv φ (⟨R.get i, ⊥⟩::Γ) (R.pack::L)}
+  : cfg R (β.lsubst Subst.Eqv.unpack.extend) (λi => (G i).lsubst Subst.Eqv.unpack.extend)
+  = gloop R.pack β (Eqv.unpack.lsubst (Subst.Eqv.fromFCFG G).vlift) := by
+  convert dinaturality_to_gloop_rec
+  · rw [Subst.Eqv.vlift_extend, Subst.Eqv.vlift_unpack]
+  · rw [Subst.Eqv.unpack_zero]
+
+-- theorem Eqv.gloop_pack_entry_rec {Γ : Ctx α ε} {R L : LCtx α}
+--   {β : Eqv φ Γ (R ++ L)} {G : Eqv φ (⟨R.pack, ⊥⟩::Γ) (R.pack::L)}
+--   : gloop R.pack (β.lsubst Subst.Eqv.pack.extend) G
+--   = cfg R β (λi => (ret (Term.Eqv.inj_n R i) ;; G).lsubst Subst.Eqv.unpack.extend)
+--   := sorry
+
+end Region
+
+end BinSyntax

DeBruijnSSA/BinSyntax/Rewrite/Term/Compose/Completeness.lean

@@ -1,5 +1,5 @@
-import DeBruijnSSA.BinSyntax.Rewrite.Term.Compose.Structural.Product
-import DeBruijnSSA.BinSyntax.Rewrite.Term.Compose.Structural.Sum
+import DeBruijnSSA.BinSyntax.Rewrite.Term.Structural.Product
+import DeBruijnSSA.BinSyntax.Rewrite.Term.Structural.Sum
 import DeBruijnSSA.BinSyntax.Rewrite.Term.Compose.Distrib
 
 namespace BinSyntax

DeBruijnSSA/BinSyntax/Rewrite/Term/Compose/Structural.lean → DeBruijnSSA/BinSyntax/Rewrite/Term/Structural.lean

@@ -1,5 +1,5 @@
-import DeBruijnSSA.BinSyntax.Rewrite.Term.Compose.Structural.Sum
-import DeBruijnSSA.BinSyntax.Rewrite.Term.Compose.Structural.Product
+import DeBruijnSSA.BinSyntax.Rewrite.Term.Structural.Sum
+import DeBruijnSSA.BinSyntax.Rewrite.Term.Structural.Product
 
 namespace BinSyntax
 

DeBruijnSSA/BinSyntax/Typing/Region/LSubst.lean

@@ -681,6 +681,17 @@ theorem Region.InS.coe_csubst {Γ : Ctx α ε} {L : LCtx α} {r : Region.InS φ
   : (r.csubst : Region.Subst φ) = r.val.csubst
   := rfl
 
+theorem Region.Subst.InS.vlift_extend_in {Γ : Ctx α ε} {L K : LCtx α} {σ : Subst.InS φ Γ L (K ++ R)}
+  : σ.extend_in.vlift (head := head) = σ.vlift.extend_in := by ext k; simp only [Set.mem_setOf_eq,
+    coe_vlift, Subst.vlift, coe_extend_in, Function.comp_apply, Subst.extend]; split <;> rfl
+
+theorem Region.Subst.InS.vlift_extend_out {Γ : Ctx α ε} {L K : LCtx α} {σ : Subst.InS φ Γ L K}
+  : σ.extend_out.vlift (head := head) = σ.vlift.extend_out (R := R) := by rfl
+
+theorem Region.Subst.InS.vlift_extend {Γ : Ctx α ε} {L K : LCtx α} {σ : Subst.InS φ Γ L K}
+  : σ.extend.vlift (head := head) = σ.vlift.extend (R := R)
+  := by rw [<-extend_in_extend_out, vlift_extend_in, vlift_extend_out, extend_in_extend_out]
+
 end RegionSubst
 
 end BinSyntax