packed_cfg_den statement

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

@@ -0,0 +1,51 @@
+import DeBruijnSSA.BinSyntax.Rewrite.Region.Compose.Sum
+import DeBruijnSSA.BinSyntax.Rewrite.Region.Compose.Product
+
+namespace BinSyntax
+
+variable [Φ: EffInstSet φ (Ty α) ε] [PartialOrder α] [SemilatticeSup ε] [OrderBot ε]
+
+namespace Region
+
+def Eqv.acast {Γ : Ctx α ε} {L : LCtx α} {X Y : Ty α} (h : X = Y)
+  : Eqv φ ((X, ⊥)::Γ) (Y::L) := (Eqv.nil (targets := L)).cast rfl (by rw [h])
+
+@[simp]
+theorem Eqv.acast_rfl {Γ : Ctx α ε} {L : LCtx α} {X : Ty α}
+  : Eqv.acast (φ := φ) (Γ := Γ) (L := L) (X := X) rfl = Eqv.nil := rfl
+
+theorem Eqv.acast_acast {Γ : Ctx α ε} {L : LCtx α} {X Y Z : Ty α} {h : X = Y} {h' : Y = Z}
+  : (Eqv.acast (φ := φ) (Γ := Γ) (L := L) h) ;; acast h' = Eqv.acast (by rw [h, h'])
+  := by cases h; cases h'; simp
+
+theorem Eqv.rtimes_acast {Γ : Ctx α ε} {L : LCtx α} {X Y : Ty α} {h : X = Y}
+  : Z ⋊ (acast (φ := φ) (Γ := Γ) (L := L) h) = acast (by rw [h])
+  := by cases h; simp [rtimes_nil]
+
+theorem Eqv.ltimes_acast {Γ : Ctx α ε} {L : LCtx α} {X Y : Ty α} {h : X = Y}
+  : (acast (φ := φ) (Γ := Γ) (L := L) h) ⋉ Z = acast (by rw [h])
+  := by cases h; simp [ltimes_nil]
+
+theorem Eqv.sum_acast {Γ : Ctx α ε} {L : LCtx α}
+  {X Y X' Y' : Ty α} {h : X = Y} {h' : X' = Y'}
+  : sum (acast (φ := φ) (Γ := Γ) (L := L) h) (acast h') = acast (by rw [h, h'])
+  := by cases h; cases h'; simp [sum_nil]
+
+theorem Eqv.sum_acast_nil {Γ : Ctx α ε} {L : LCtx α}
+  {X Y : Ty α} {h : X = Y}
+  : sum (acast (φ := φ) (Γ := Γ) (L := L) h) (nil (ty := X')) = acast (by rw [h])
+  := by cases h; simp [sum_nil]
+
+theorem Eqv.sum_nil_acast {Γ : Ctx α ε} {L : LCtx α}
+  {X Y : Ty α} {h : X = Y}
+  : sum (nil (ty := X')) (acast (φ := φ) (Γ := Γ) (L := L) h) = acast (by rw [h])
+  := by cases h; simp [sum_nil]
+
+theorem Eqv.sum_acast_inv {Γ : Ctx α ε} {L : LCtx α}
+  {X Y X' Y' : Ty α} {h : X.coprod Y = X'.coprod Y'}
+  : (acast (φ := φ) (Γ := Γ) (L := L) h) = sum (acast (by cases h; rfl)) (acast (by cases h; rfl))
+  := by cases h; simp [sum_nil]
+
+end Region
+
+end BinSyntax

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

@@ -1,6 +1,7 @@
 import DeBruijnSSA.BinSyntax.Rewrite.Region.Structural
 import DeBruijnSSA.BinSyntax.Rewrite.Region.Compose.Functor
 import DeBruijnSSA.BinSyntax.Rewrite.Region.Compose.Elgot
+import DeBruijnSSA.BinSyntax.Rewrite.Region.Compose.Cast
 import DeBruijnSSA.BinSyntax.Rewrite.Term.Structural.Distrib
 
 namespace BinSyntax
@@ -148,14 +149,11 @@ theorem Eqv.packed_case_den {Γ : Ctx α ε} {R : LCtx α}
 
 theorem Eqv.packed_cfg_den {Γ : Ctx α ε} {L R : LCtx α} {β : Eqv φ Γ (R ++ L)} {G}
   : (cfg R β G).packed (Δ := Δ)
-  = ret Term.Eqv.split ;; _ ⋊ (β.packed ;; ret Term.Eqv.pack_app) ;; distl_inv
-  ;; coprod pi_r (fixpoint (ret Term.Eqv.distl_pack ;; unpack.lsubst (Subst.Eqv.fromFCFG (λi =>
-    ret (Term.Eqv.nil.cast
-      (V := ((R.dist Γ.pack).get i, ⊥))
-      (V' := (Γ.pack.prod (R.get (i.cast R.length_dist)), ⊥)) rfl (by simp [R.getElem_dist]))
-    ;; ret Term.Eqv.split ⋉ _
-    ;; assoc
-    ;; _ ⋊ ((G (i.cast R.length_dist)).packed ;; ret Term.Eqv.pack_app)
-    ;; sorry
-  ))))
+  = ret Term.Eqv.split ;; _ ⋊ β.packed ;; fixpoint (
+    _ ⋊ ret Term.Eqv.pack_app ;; distl_inv ;; sum pi_r (
+      ret Term.Eqv.distl_pack ;; pack_coprod
+        (λi => acast (R.get_dist (i := i)) ;; ret Term.Eqv.split ⋉ _ ;; assoc
+            ;; _ ⋊ (G (i.cast R.length_dist)).packed
+        )
+    ))
   := sorry

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

@@ -11,20 +11,20 @@ namespace Region
 
 open Term.Eqv
 
-def Eqv.coprod {A B C : Ty α} {Γ : Ctx α ε} {L : LCtx α}
-  (l : Eqv φ (⟨A, ⊥⟩::Γ) (C::L)) (r : Eqv φ (⟨B, ⊥⟩::Γ) (C::L))
-  : Eqv φ (⟨A.coprod B, ⊥⟩::Γ) (C::L)
+def Eqv.coprod {A B : Ty α} {Γ : Ctx α ε} {L : LCtx α}
+  (l : Eqv φ (⟨A, ⊥⟩::Γ) L) (r : Eqv φ (⟨B, ⊥⟩::Γ) L)
+  : Eqv φ (⟨A.coprod B, ⊥⟩::Γ) L
   := case (var 0 Ctx.Var.shead) l.vwk1 r.vwk1
 
-theorem Eqv.lwk_slift_coprod {A B C : Ty α} {Γ : Ctx α ε} {L K : LCtx α}
-  {ρ : L.InS K} {l : Eqv φ (⟨A, ⊥⟩::Γ) (C::L)} {r : Eqv φ (⟨B, ⊥⟩::Γ) (C::L)}
-  : (l.coprod r).lwk ρ.slift = (l.lwk ρ.slift).coprod (r.lwk ρ.slift)
+theorem Eqv.lwk_coprod {A B : Ty α} {Γ : Ctx α ε} {L K : LCtx α}
+  {ρ : L.InS K} {l : Eqv φ (⟨A, ⊥⟩::Γ) L} {r : Eqv φ (⟨B, ⊥⟩::Γ) L}
+  : (l.coprod r).lwk ρ = (l.lwk ρ).coprod (r.lwk ρ)
   := by simp only [coprod, lwk_case, vwk1_lwk]
 
 theorem Eqv.lwk1_coprod {A B C : Ty α} {Γ : Ctx α ε} {L : LCtx α}
   {l : Eqv φ (⟨A, ⊥⟩::Γ) (C::L)} {r : Eqv φ (⟨B, ⊥⟩::Γ) (C::L)}
   : (l.coprod r).lwk1 (inserted := inserted) = (l.lwk1).coprod (r.lwk1)
-  := by simp only [lwk1, <-LCtx.InS.slift_wk0, lwk_slift_coprod]
+  := by simp only [lwk1, <-LCtx.InS.slift_wk0, lwk_coprod]
 
 theorem Eqv.vwk_slift_coprod {A B C : Ty α} {Γ Δ : Ctx α ε} {L : LCtx α}
   {ρ : Γ.InS Δ}
@@ -38,6 +38,13 @@ theorem Eqv.vwk1_coprod {A B C : Ty α} {Γ : Ctx α ε} {L : LCtx α}
   : (l.coprod r).vwk1 (inserted := inserted) = l.vwk1.coprod r.vwk1 := by
   simp only [vwk1, <-Ctx.InS.lift_wk0, vwk_slift_coprod]
 
+theorem Eqv.lsubst_vlift_coprod {A B : Ty α} {Γ : Ctx α ε} {L K : LCtx α}
+  {σ : Subst.Eqv φ Γ L K} {l : Eqv φ (⟨A, ⊥⟩::Γ) L} {r : Eqv φ (⟨B, ⊥⟩::Γ) L}
+  : (l.coprod r).lsubst σ.vlift = (l.lsubst σ.vlift).coprod (r.lsubst σ.vlift)
+  := by
+  simp only [coprod, lsubst_case, vwk1, vwk_lsubst, <-Subst.Eqv.vwk_wk0, Subst.Eqv.vwk_vwk]
+  rfl
+
 theorem Eqv.ret_of_coprod {A B C : Ty α} {Γ : Ctx α ε} {L : LCtx α}
   {l : Term.Eqv φ (⟨A, ⊥⟩::Γ) (C, ⊥)} {r : Term.Eqv φ (⟨B, ⊥⟩::Γ) (C, ⊥)}
   : ret (targets := L) (l.coprod r) = (ret l).coprod (ret r) := by
@@ -146,7 +153,7 @@ def Eqv.sum {A B C D : Ty α} {Γ : Ctx α ε} {L : LCtx α}
 theorem Eqv.lwk_slift_sum {A B C D : Ty α} {Γ : Ctx α ε} {L K : LCtx α}
   {ρ : L.InS K} {l : Eqv φ (⟨A, ⊥⟩::Γ) (C::L)} {r : Eqv φ (⟨B, ⊥⟩::Γ) (D::L)}
   : (l.sum r).lwk ρ.slift = (l.lwk ρ.slift).sum (r.lwk ρ.slift)
-  := by simp only [sum, lwk_slift_coprod, lwk_slift_seq]; rfl
+  := by simp only [sum, lwk_coprod, lwk_slift_seq]; rfl
 
 theorem Eqv.lwk1_sum {A B C D : Ty α} {Γ : Ctx α ε} {L : LCtx α}
   {l : Eqv φ (⟨A, ⊥⟩::Γ) (C::L)} {r : Eqv φ (⟨B, ⊥⟩::Γ) (D::L)}

DeBruijnSSA/BinSyntax/Rewrite/Region/Eqv.lean

@@ -819,6 +819,13 @@ theorem Eqv.vwk1_let2 {L : LCtx α}
   apply Eqv.eq_of_reg_eq
   simp [Nat.liftnWk_succ]
 
+theorem Eqv.vsubst0_var0_vwk1 {Γ : Ctx α ε} {L : LCtx α} {r : Eqv φ (head::Γ) L}
+  : (r.vwk1 (inserted := _)).vsubst (Term.Eqv.var 0 Ctx.Var.shead).subst0 = r := by
+  induction r using Quotient.inductionOn
+  apply eq_of_reg_eq
+  simp
+  exact Region.vsubst0_var0_vwk1 _
+
 def Eqv.vswap01
   {Γ : Ctx α ε} {L : LCtx α} (r : Eqv φ (left::right::Γ) L)
   : Eqv φ (right::left::Γ) L := Eqv.vwk Ctx.InS.swap01 r

DeBruijnSSA/BinSyntax/Rewrite/Region/LSubst.lean

@@ -459,6 +459,16 @@ theorem Subst.Eqv.vwk_quot {Γ Δ : Ctx α ε} {L K : LCtx α}
   {ρ : Γ.InS Δ} {σ : Subst.InS φ Δ L K}
   : vwk ρ ⟦σ⟧ = ⟦σ.vwk ρ⟧ := rfl
 
+theorem Subst.Eqv.vwk_wk0 {Γ : Ctx α ε} {σ : Subst.Eqv φ Γ L K}
+  : (σ.vwk <| Ctx.InS.wk0 (head := head)) = σ.vlift := by
+  induction σ using Quotient.inductionOn; rfl
+
+theorem Subst.Eqv.vwk_vwk {Γ Δ Ξ : Ctx α ε} {L K : LCtx α}
+  {ρ : Γ.InS Δ} {τ : Δ.InS Ξ} {σ : Subst.Eqv φ Ξ L K}
+  : (σ.vwk τ).vwk ρ = σ.vwk (ρ.comp τ) := by
+  induction σ using Quotient.inductionOn
+  simp [Subst.InS.vwk_vwk]
+
 theorem Eqv.vwk_lsubst {Γ Δ : Ctx α ε}
   {L K : LCtx α} {σ : Subst.Eqv φ Δ L K} {ρ : Γ.InS Δ}
   {r : Eqv φ Δ L}
@@ -717,6 +727,13 @@ theorem Subst.Eqv.get_fromFCFG {Γ : Ctx α ε} {L K : LCtx α}
   : (fromFCFG G).get i = G i
   := by induction G using Eqv.choiceInduction; rw [Subst.Eqv.fromFCFG_quot]; simp
 
+theorem Subst.Eqv.fromFCFG_get {Γ : Ctx α ε} {L K : LCtx α} {σ : Subst.Eqv φ Γ L K}
+  : (fromFCFG σ.get) = σ := by ext k; simp [Subst.Eqv.get_fromFCFG]
+
+theorem Subst.Eqv.get_fromFCFG' {Γ : Ctx α ε} {L K : LCtx α}
+  {G : ∀i : Fin L.length, Region.Eqv φ ((L.get i, ⊥)::Γ) K}
+  : (fromFCFG G).get = G := funext (λ_ => get_fromFCFG)
+
 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)

DeBruijnSSA/BinSyntax/Rewrite/Region/Structural.lean

@@ -119,16 +119,28 @@ theorem Eqv.packed_case {Γ : Ctx α ε} {R : LCtx α}
     (let1 (pair (var 1 (by simp)) (var 0 Ctx.Var.shead)) s.packed) := by
   simp only [packed, packed_out_case, packed_in_case]
 
-theorem Eqv.packed_cfg {Γ : Ctx α ε} {L R : LCtx α} {β : Eqv φ Γ (R ++ L)} {G}
+theorem Eqv.packed_cfg_unpack {Γ : Ctx α ε} {L R : LCtx α} {β : Eqv φ Γ (R ++ L)} {G}
   : (cfg R β G).packed (Δ := Δ)
-  = gloop R.pack β.packed.unpacked_app_out
+  = gloop R.pack
+      β.packed.unpacked_app_out
       (unpack.lsubst (Subst.Eqv.fromFCFG (λi =>
         (let1 (pair (var 2 (by simp)) (var 0 Ctx.Var.shead)) (G i).packed.unpacked_app_out)))) := by
-  rw [packed_def', packed_in_cfg, packed_out_cfg_gloop, <-packed_def']
+  rw [packed_def', packed_in_cfg, packed_out_cfg_gloop_unpack, <-packed_def']
   congr; funext i
   rw [vwk1_unpacked_app_out, packed_out_let1, <-packed_def', <-unpacked_app_out_let1]
   simp
 
+theorem Eqv.packed_cfg {Γ : Ctx α ε} {L R : LCtx α} {β : Eqv φ Γ (R ++ L)} {G}
+  : (cfg R β G).packed (Δ := Δ)
+  = gloop R.pack
+      β.packed.unpacked_app_out
+      (pack_coprod
+        (λi => (let1 (pair (var 1 (by simp)) (var 0 Ctx.Var.shead)) (G i).packed.unpacked_app_out)))
+  := by
+  rw [packed_def', packed_in_cfg, packed_out_cfg_gloop, <-packed_def']
+  congr; funext i
+  rw [packed_out_let1, <-packed_def', unpacked_app_out_let1]
+
 end Region
 
 end BinSyntax

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

@@ -25,18 +25,67 @@ theorem Eqv.unpack_def {Γ : Ctx α ε} {R : LCtx α}
     simp [
       Region.unpack, Region.nil, Region.ret, Region.lwk0, Region.vwk_lwk, Region.vwk_lift_unpack]
 
--- def Eqv.pack_case {Γ : Ctx α ε} {R : LCtx α} {X : Ty α}
---   (r : Eqv φ ((X.prod R, ⊥)::Γ) (R.dist X, e)) : Eqv φ ((R.dist X, ⊥)::Γ) (R.pack, e) :=
---   case (Term.Eqv.dist X)
---     (br (List.length R) Term.Eqv.pi_r (by simp))
---     (lwk_id LCtx.Wkn.id_right_dist r)
-
-def Eqv.pack_coprod {Γ : Ctx α ε} {R : LCtx α}
-  (G : (i : Fin R.length) → Eqv φ (⟨R.get i, ⊥⟩::Γ) (A::L)) : Eqv φ ((R.pack, ⊥)::Γ) (A::L) :=
+def Eqv.pack_case {Γ : Ctx α ε} {R L : LCtx α}
+  (a : Term.Eqv φ Γ (R.pack, e)) (G : (i : Fin R.length) → Eqv φ (⟨R.get i, ⊥⟩::Γ) L)
+  : Eqv φ Γ L := match R with
+  | [] => let1 a loop
+  | _::R => case a
+    (pack_case (e := e) Term.Eqv.nil (λi => (G i.succ).vwk1))
+    (G (0 : Fin (R.length + 1)))
+
+theorem Eqv.vwk_pack_case {Γ : Ctx α ε} {R L : LCtx α}
+  {a : Term.Eqv φ Δ (R.pack, e)} {G : (i : Fin R.length) → Eqv φ (⟨R.get i, ⊥⟩::Δ) L}
+  {ρ : Γ.InS Δ}
+  : (pack_case a G).vwk ρ = pack_case (a.wk ρ) (λi => (G i).vwk ρ.slift) := by
+  induction R generalizing Γ Δ with
+  | nil => simp [pack_case]
+  | cons A R I =>
+    simp only [pack_case, vwk_case, I]
+    congr; funext i; simp only [vwk1, vwk_vwk]
+    congr 1; ext k; cases k <;> rfl
+
+theorem Eqv.vwk1_pack_case {Γ : Ctx α ε} {R L : LCtx α}
+  (a : Term.Eqv φ (V::Γ) (R.pack, e)) (G : (i : Fin R.length) → Eqv φ (⟨R.get i, ⊥⟩::V::Γ) L)
+  : (pack_case a G).vwk1 (inserted := inserted) = pack_case (φ := φ) a.wk1 (λi => (G i).vwk2) := by
+  simp only [vwk1, <-Ctx.InS.lift_wk0, vwk_pack_case]
+  simp only [Ctx.InS.lift_wk0, Ctx.InS.lift_wk1]; rfl
+
+-- TODO: vsubst_pack_case, lwk_pack_case, lsubst_pack_case
+
+def Eqv.pack_coprod {Γ : Ctx α ε} {R L : LCtx α}
+  (G : (i : Fin R.length) → Eqv φ (⟨R.get i, ⊥⟩::Γ) L) : Eqv φ ((R.pack, ⊥)::Γ) L :=
   match R with
-  | [] => zero
+  | [] => loop
   | _::R => coprod (pack_coprod (λi => G i.succ)) (G (0 : Fin (R.length + 1)))
 
+theorem Eqv.pack_case_nil_vwk1 {Γ : Ctx α ε} {R L : LCtx α}
+  (G : (i : Fin R.length) → Eqv φ (⟨R.get i, ⊥⟩::Γ) L)
+  : pack_case (e := e) Term.Eqv.nil (λi => (G i).vwk1) = pack_coprod G := by induction R with
+  | nil => rw [
+    pack_coprod, pack_case, <-Term.Eqv.wk_eff_nil (h := bot_le), let1_wk_eff,
+    let1_beta, vsubst_loop
+  ]
+  | cons A R I =>
+    rw [
+      pack_case, pack_coprod, <-I, coprod, <-Term.Eqv.wk_eff_nil (h := bot_le), case_wk_eff,
+      vwk1_pack_case]
+    simp only [vwk1_vwk2]
+    rfl
+
+-- TODO: vwk_lift_pack_coprod, vsubst_lift_pack_coprod, lwk_pack_coprod, lsubst_pack_coprod
+
+theorem Eqv.pack_coprod_empty {Γ : Ctx α ε} {L : LCtx α}
+  (G : (i : Fin 0) → Eqv φ (⟨[].get i, ⊥⟩::Γ) L) : (pack_coprod (R := []) G) = loop := rfl
+
+theorem Eqv.pack_coprod_cons {Γ : Ctx α ε} {R : LCtx α} {L : LCtx α}
+  (G : (i : Fin (R.length + 1)) → Eqv φ (⟨(A::R).get i, ⊥⟩::Γ) L)
+  : (pack_coprod (R := A::R) G) = coprod (pack_coprod (λi => G i.succ)) (G (0 : Fin (R.length + 1)))
+  := rfl
+
+theorem Eqv.pack_coprod_zero {Γ : Ctx α ε} {L : LCtx α}
+  (G : (i : Fin 0) → Eqv φ (⟨[].get i, ⊥⟩::Γ) (A::L)) : (pack_coprod (R := []) G) = zero := by
+  rw [pack_coprod_empty]; apply Eqv.zero_eq
+
 @[simp]
 theorem Eqv.vwk_lift_unpack {Γ Δ : Ctx α ε} {R : LCtx α} (ρ : Γ.InS Δ)
   : Eqv.vwk (ρ.lift (le_refl _)) (Eqv.unpack (φ := φ) (R := R)) = unpack := by
@@ -57,6 +106,32 @@ theorem Eqv.vsubst_lift_unpack {Γ Δ : Ctx α ε} {R : LCtx α} (σ : Term.Subs
   apply Eqv.eq_of_reg_eq
   simp
 
+theorem Eqv.lsubst_vlift_fromFCFG_unpack {Γ : Ctx α ε} {L K : LCtx α}
+  {G : (i : Fin L.length) → Eqv φ (⟨L.get i, ⊥⟩::Γ) K}
+  : Eqv.lsubst (Subst.Eqv.fromFCFG G).vlift Eqv.unpack = Eqv.pack_coprod G := by
+  induction L with
+  | nil => simp [unpack, pack_coprod]
+  | cons A L I =>
+    simp [unpack, pack_coprod, lsubst_vlift_coprod]
+    rw [<-I, lwk0, <-lsubst_toSubstE, lsubst_lsubst]
+    congr
+    · ext k; simp only [List.get_eq_getElem, Subst.Eqv.get_comp, Subst.Eqv.get_toSubstE,
+      Set.mem_setOf_eq, LCtx.InS.coe_wk0, Nat.succ_eq_add_one, lsubst_br, List.length_cons, id_eq,
+      List.getElem_cons_succ, Subst.Eqv.get_vlift, Subst.Eqv.get_fromFCFG, vwk_id_eq,
+      vsubst0_var0_vwk1]; rfl
+    · simp [<-br_zero_eq_ret, <-ret_nil, Subst.Eqv.get_fromFCFG, Term.Eqv.nil, vsubst0_var0_vwk1]
+
+theorem Eqv.lsubst_vlift_unpack {Γ : Ctx α ε} {L K : LCtx α} (σ : Subst.Eqv φ Γ L K)
+  : Eqv.lsubst σ.vlift Eqv.unpack = Eqv.pack_coprod σ.get := by
+  rw [<-Subst.Eqv.fromFCFG_get (σ := σ), lsubst_vlift_fromFCFG_unpack, Subst.Eqv.fromFCFG_get]
+
+theorem Eqv.lsubst_fromFCFG_vwk1_unpack {Γ : Ctx α ε} {R L : LCtx α}
+  {G : (i : Fin R.length) → Eqv φ (⟨R.get i, ⊥⟩::Γ) L}
+  : Eqv.lsubst (Subst.Eqv.fromFCFG (λi => (G i).vwk1)) Eqv.unpack
+  = Eqv.pack_coprod G := by
+  convert Eqv.lsubst_vlift_fromFCFG_unpack
+  ext l; simp [Subst.Eqv.get_fromFCFG]
+
 def Subst.Eqv.unpack {Γ : Ctx α ε} {R : LCtx α} : Subst.Eqv φ Γ [R.pack] R
   := Region.Eqv.unpack.csubst
 
@@ -285,7 +360,7 @@ theorem Eqv.lsubst_pack_append_vlift_unpack {Γ : Ctx α ε} {L R : LCtx α}
         funext k
         simp only [Subst.comp, Region.lsubst, Subst.vlift, Nat.succ_eq_add_one, Function.comp_apply,
           Subst.liftn, add_lt_add_iff_right, Region.lwk, zero_add, Nat.reduceSubDiff,
-          vsubst0_var0_vwk1, Subst.vwk1_comp_fromLwk, vwk2_vwk1, lsubst_fromLwk]
+          Region.vsubst0_var0_vwk1, Subst.vwk1_comp_fromLwk, vwk2_vwk1, lsubst_fromLwk]
         split <;> rfl
       · simp [
           lwk0, Term.Eqv.seq, let1_let1, Term.Eqv.sum, Term.Eqv.coprod, Term.Eqv.wk2, Term.Eqv.nil,
@@ -319,6 +394,12 @@ theorem Eqv.lsubst_pack_append_vlift_unpack {Γ : Ctx α ε} {L R : LCtx α}
       apply eq_of_reg_eq
       simp
 
+theorem Eqv.pack_coprod_pack_append {Γ : Ctx α ε} {L R : LCtx α}
+  : pack_coprod (Subst.Eqv.liftn_append R Subst.Eqv.pack).get
+  = unpack_right_out (φ := φ) (Γ := Γ) (R := R) (L := L) := by
+  convert lsubst_pack_append_vlift_unpack
+  rw [lsubst_vlift_unpack]
+
 theorem Eqv.lsubst_pack_append_unpack {Γ : Ctx α ε} {L R : LCtx α}
   : lsubst (Subst.Eqv.liftn_append R Subst.Eqv.pack) (unpack (φ := φ) (Γ := Γ) (R := R ++ L))
   = unpack_right_out := by
@@ -433,10 +514,11 @@ theorem Eqv.extend_unpack_unpacked_app_out
   : r.unpacked_app_out.lsubst Subst.Eqv.unpack.extend = r.unpacked_right_out := by
   rw [unpacked_app_out, lsubst_lsubst, Subst.Eqv.extend_unpack_comp_unpack_app_out]; rfl
 
-theorem Eqv.packed_out_cfg_gloop {Γ : Ctx α ε} {R L : LCtx α}
+theorem Eqv.packed_out_cfg_gloop_unpack {Γ : Ctx α ε} {R L : LCtx α}
   {β : Eqv φ Γ (R ++ L)} {G : (i : Fin R.length) → Eqv φ (⟨R.get i, ⊥⟩::Γ) (R ++ L)}
   : (cfg R β G).packed_out
-  = gloop R.pack β.packed_out.unpacked_app_out
+  = gloop R.pack
+      β.packed_out.unpacked_app_out
       (unpack.lsubst (Subst.Eqv.fromFCFG (λi => (G i).packed_out.unpacked_app_out.vwk1))) := calc
   _ = (cfg R (β.packed_out.unpacked_app_out.lsubst Subst.Eqv.unpack.extend)
               (λi => (G i).packed_out.unpacked_app_out.lsubst Subst.Eqv.unpack.extend.vlift))
@@ -447,6 +529,14 @@ theorem Eqv.packed_out_cfg_gloop {Γ : Ctx α ε} {R L : LCtx α}
     · ext k; simp [Subst.Eqv.get_fromFCFG]
     · simp [Subst.Eqv.unpack]
 
+theorem Eqv.packed_out_cfg_gloop {Γ : Ctx α ε} {R L : LCtx α}
+  {β : Eqv φ Γ (R ++ L)} {G : (i : Fin R.length) → Eqv φ (⟨R.get i, ⊥⟩::Γ) (R ++ L)}
+  : (cfg R β G).packed_out
+  = gloop R.pack
+    β.packed_out.unpacked_app_out
+    (pack_coprod (λi => (G i).packed_out.unpacked_app_out))
+  := by rw [packed_out_cfg_gloop_unpack, lsubst_fromFCFG_vwk1_unpack]
+
 -- theorem Eqv.packed_out_gloop {Γ : Ctx α ε} {R L : LCtx α}
 --   {β : Eqv φ Γ (A::L)} {G : Eqv φ (⟨A, ⊥⟩::Γ) (A::L)}
 --   : (gloop A β G).packed_out

DeBruijnSSA/BinSyntax/Typing/Region/LSubst.lean

@@ -533,6 +533,11 @@ theorem Region.Subst.InS.get_vwk {Γ Δ : Ctx α ε}
   : (σ.vwk ρ).get i = (σ.get i).vwk ρ.slift
   := rfl
 
+theorem Region.Subst.InS.vwk_vwk {Γ Δ Ξ : Ctx α ε}
+  {ρ : Γ.InS Δ} {τ : Δ.InS Ξ} {σ : Region.Subst.InS φ Ξ L K}
+  : (σ.vwk τ).vwk ρ = σ.vwk (ρ.comp τ)
+  := by ext; simp [Region.vwk_vwk, Nat.liftWk_comp]
+
 def Region.Subst.InS.vsubst {Γ Δ : Ctx α ε}
   (ρ : Term.Subst.InS φ Γ Δ) (σ : Region.Subst.InS φ Δ L K)
   : Region.Subst.InS φ Γ L K