Further Elgotwork

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

@@ -159,18 +159,74 @@ theorem Eqv.packed_case_den {Γ : Ctx α ε} {R : LCtx α}
 
 open Term.Eqv
 
+-- theorem Eqv.packed_cfg_den {Γ : Ctx α ε} {L R : LCtx α} {β : Eqv φ Γ (R ++ L)} {G}
+--   : (cfg R β G).packed (Δ := Δ)
+--   = 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
+--         ))) := by
+--   -- rw [
+--   --   packed_cfg_unpack, letc_to_vwk1, letc_vwk1_den, ret_seq, <-vsubst_packed_out,
+--   --   <-vwk1_packed_out, <-ret_seq
+--   -- ]
+--   -- simp only [seq_assoc]
+--   -- congr 1
+--   sorry
+
+theorem Eqv.unpacked_app_out_eq_left_exit {Γ : Ctx α ε} {R L : LCtx α}
+  {r : Eqv φ ((A, ⊥)::Γ) [(R ++ L).pack]} : r.unpacked_app_out
+  = (r ;; ret Term.Eqv.pack_app).lwk1 ;; left_exit
+  := by
+  rw [seq, seq, lwk1, <-lsubst_toSubstE, lsubst_lsubst, lsubst_lsubst, unpacked_app_out]
+  congr; ext k; cases k using Fin.elim1
+  simp only [Fin.isValue, List.get_eq_getElem, List.length_singleton, Fin.val_zero,
+    List.getElem_cons_zero, Subst.Eqv.unpack_app_out, unpack_app_out, csubst_get, cast_rfl,
+    left_exit, List.getElem_cons_succ, vwk1_case, wk1_var0, List.length_cons, Fin.zero_eta, vwk2_br,
+    wk2_var0, vwk1_br, wk1_pack_app, Subst.Eqv.get_comp, get_alpha0, List.length_nil, Fin.val_succ,
+    Fin.cases_zero, lsubst_br, Subst.Eqv.get_vlift, Subst.Eqv.get_toSubstE, Set.mem_setOf_eq,
+    Fin.coe_fin_one, LCtx.InS.coe_wk1, Nat.liftWk_zero, Nat.reduceAdd, zero_add, vwk_id_eq,
+    vsubst_case, var0_subst0, wk_res_self, vsubst_br, subst_lift_var_zero, Nat.add_zero,
+    Nat.zero_eq]
+  rfl
+
 theorem Eqv.packed_cfg_den {Γ : Ctx α ε} {L R : LCtx α} {β : Eqv φ Γ (R ++ L)} {G}
   : (cfg R β G).packed (Δ := Δ)
-  = 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
-        ))) := by
-  rw [
-    packed_cfg_unpack, letc_to_vwk1, letc_vwk1_den, ret_seq, <-vsubst_packed_out,
-    <-vwk1_packed_out, <-ret_seq
-  ]
-  simp only [seq_assoc]
+  = (ret Term.Eqv.split ;; _ ⋊ (β.packed ;; ret Term.Eqv.pack_app) ;; distl_inv ;; sum pi_r nil)
+    ;; coprod nil (
+      fixpoint (
+        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 ;; ret Term.Eqv.pack_app)
+              ;; distl_inv
+              ;; sum pi_r nil
+          )
+      )
+    )
+   := by
+  rw [packed_cfg_split_vwk1, fixpoint_def', letc_vwk1_den]
   congr 1
-  sorry
+  · rw [ret_seq, <-vsubst_packed_out, <-vwk1_packed_out, <-ret_seq]
+    simp only [seq_assoc]
+    congr 1
+    simp [distl_inv_eq_ret, ret_seq, sum, coprod, vwk1_vwk2]
+    simp [
+      vwk1_seq, Term.Eqv.distl_inv, vsubst_lift_seq, rtimes, packed_out_let2, let2_seq,
+      vwk1_unpacked_app_out, wk1_coprod, wk1_let2, <-Ctx.InS.lift_lift, wk_lift_coprod,
+      Nat.liftnWk
+    ]
+    congr 1
+    conv => rhs; rw [<-ret, case_let2, seq_assoc]; rhs; rw [ret_seq]
+    simp [
+      vwk1_let2, <-Term.Subst.Eqv.lift_lift, vsubst_lift_coprod, vwk2_seq, vwk1_seq, vwk3,
+      vwk_lift_seq, vsubst_lift_seq, <-Ctx.InS.lift_wk2, Nat.liftnWk, Term.Eqv.coprod, let2_pair,
+      let1_beta, case_case
+    ]
+    simp [
+      case_inl, case_inr
+    ]
+    sorry
+  · rw [fixpoint_def']
+    congr 5
+    sorry

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

@@ -209,6 +209,19 @@ theorem Eqv.runit_eq_ret {ty : Ty α} {Γ : Ctx α ε} {L : LCtx α}
 theorem Eqv.vwk1_pi_l {Γ : Ctx α ε} {L : LCtx α}
   : (pi_l (φ := φ) (A := A) (B := B) (Γ := Γ) (L := L)).vwk1 (inserted := inserted) = pi_l := rfl
 
+@[simp]
+theorem Eqv.vwk2_pi_l {Γ : Ctx α ε} {L : LCtx α}
+  : (pi_l (φ := φ) (A := A) (B := B) (Γ := V::Γ) (L := L)).vwk2 (inserted := inserted) = pi_l := rfl
+
+@[simp]
+theorem Eqv.vwk_lift_pi_l {Γ Δ : Ctx α ε} {L : LCtx α} {ρ : Ctx.InS Γ Δ}
+  : (pi_l (φ := φ) (A := A) (B := B) (L := L)).vwk (ρ.lift (le_refl _)) = pi_l := rfl
+
+@[simp]
+theorem Eqv.vsubst_lift_pi_l {Γ Δ : Ctx α ε} {L : LCtx α} {ρ : Term.Subst.Eqv φ Γ Δ}
+  : (pi_l (φ := φ) (A := A) (B := B) (L := L)).vsubst (ρ.lift (le_refl _)) = pi_l := by
+  induction ρ using Quotient.inductionOn; rfl
+
 theorem Eqv.ret_pair_pi_l {Γ : Ctx α ε} {L : LCtx α} {A B : Ty α}
   {a : Term.Eqv φ ((X, ⊥)::Γ) (A, ⊥)} {b : Term.Eqv φ ((X, ⊥)::Γ) (B, ⊥)}
   : ret (targets := L) (a.pair b) ;; pi_l = ret a
@@ -259,6 +272,19 @@ theorem Eqv.lunit_eq_ret {ty : Ty α} {Γ : Ctx α ε} {L : LCtx α}
 theorem Eqv.vwk1_pi_r {Γ : Ctx α ε} {L : LCtx α}
   : (pi_r (φ := φ) (A := A) (B := B) (Γ := Γ) (L := L)).vwk1 (inserted := inserted) = pi_r := rfl
 
+@[simp]
+theorem Eqv.vwk2_pi_r {Γ : Ctx α ε} {L : LCtx α}
+  : (pi_r (φ := φ) (A := A) (B := B) (Γ := V::Γ) (L := L)).vwk2 (inserted := inserted) = pi_r := rfl
+
+@[simp]
+theorem Eqv.vwk_lift_pi_r {Γ Δ : Ctx α ε} {L : LCtx α} {ρ : Ctx.InS Γ Δ}
+  : (pi_r (φ := φ) (A := A) (B := B) (L := L)).vwk (ρ.lift (le_refl _)) = pi_r := rfl
+
+@[simp]
+theorem Eqv.vsubst_lift_pi_r {Γ Δ : Ctx α ε} {L : LCtx α} {ρ : Term.Subst.Eqv φ Γ Δ}
+  : (pi_r (φ := φ) (A := A) (B := B) (L := L)).vsubst (ρ.lift (le_refl _)) = pi_r := by
+  induction ρ using Quotient.inductionOn; rfl
+
 theorem Eqv.ret_pair_pi_r {Γ : Ctx α ε} {L : LCtx α} {A B : Ty α}
   {a : Term.Eqv φ ((X, ⊥)::Γ) (A, ⊥)} {b : Term.Eqv φ ((X, ⊥)::Γ) (B, ⊥)}
   : ret (targets := L) (a.pair b) ;; pi_r = ret b

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

@@ -949,3 +949,27 @@ theorem Eqv.loop_seq {Γ : Ctx α ε} {L : LCtx α} {r : Eqv φ ((B, ⊥)::Γ) (
   : loop (Γ := (A, ⊥)::Γ) (L := B::L) ;; r = loop := by
   induction r using Quotient.inductionOn
   simp [loop_def, Region.InS.append_def]
+
+theorem Eqv.lsubst_vlift_ret_seq {Γ : Ctx α ε} {L K : LCtx α}
+  {σ : Subst.Eqv φ Γ (C::L) K} {a : Term.Eqv φ (⟨A, ⊥⟩::Γ) ⟨B, ⊥⟩} {r : Eqv φ (⟨B, ⊥⟩::Γ) (C::L)}
+  : (ret a ;; r).lsubst σ.vlift = vsubst a.subst0 (r.lsubst σ.vlift).vwk1 := by
+  induction a using Quotient.inductionOn
+  induction r using Quotient.inductionOn
+  induction σ using Quotient.inductionOn
+  apply Eqv.eq_of_reg_eq
+  simp only [Set.mem_setOf_eq, InS.lsubst_br, List.length_cons, Fin.zero_eta, List.get_eq_getElem,
+    Fin.val_zero, List.getElem_cons_zero, InS.coe_lsubst, Subst.InS.coe_vlift, InS.coe_vsubst,
+    Term.InS.coe_subst0, InS.coe_vwk_id, Subst.InS.coe_get, InS.coe_alpha0, InS.coe_vwk,
+    Ctx.InS.coe_wk1, ← Region.vsubst_fromWk, Region.vsubst_vsubst, Term.liftWk_succ_comp_subst0]
+  simp only [Subst.vlift, Region.vsubst_lsubst]
+  congr 1
+  · funext k;
+    simp only [Region.vwk1, ← Region.vsubst_fromWk, Function.comp_apply, Region.vsubst_vsubst]
+    congr
+    funext j; cases j <;> rfl
+  · simp [Region.alpha, Term.alpha, Region.vsubst_vsubst]
+
+theorem Eqv.lsubst_vlift_ret_seq' {Γ : Ctx α ε} {L K : LCtx α}
+  {σ : Subst.Eqv φ Γ (C::L) (C'::K)} {a : Term.Eqv φ (⟨A, ⊥⟩::Γ) ⟨B, ⊥⟩} {r : Eqv φ (⟨B, ⊥⟩::Γ) (C::L)}
+  : (ret a ;; r).lsubst σ.vlift = ret a ;; r.lsubst σ.vlift := by
+  rw [lsubst_vlift_ret_seq, ret_seq]

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

@@ -113,10 +113,28 @@ def Eqv.inj_l {A B : Ty α} {Γ : Ctx α ε} {L : LCtx α}
 theorem Eqv.inj_l_eq_ret {A B : Ty α} {Γ : Ctx α ε} {L : LCtx α}
   : Eqv.inj_l (φ := φ) (A := A) (B := B) (Γ := Γ) (L := L) = ret Term.Eqv.inj_l := rfl
 
+@[simp]
 theorem Eqv.vwk1_inj_l {A B : Ty α} {Γ : Ctx α ε} {L : LCtx α}
   : (inj_l (φ := φ) (A := A) (B := B) (Γ := Γ) (L := L)).vwk1 (inserted := inserted)
   = inj_l := rfl
 
+@[simp]
+theorem Eqv.vwk2_inj_l {A B : Ty α} {Γ : Ctx α ε} {L : LCtx α}
+  : (inj_l (φ := φ) (A := A) (B := B) (Γ := V::Γ) (L := L)).vwk2 (inserted := inserted)
+  = inj_l := rfl
+
+@[simp]
+theorem Eqv.vwk_lift_inj_l {A B : Ty α} {Γ Δ : Ctx α ε} {L : LCtx α}
+  {ρ : Γ.InS Δ}
+  : (inj_l (φ := φ) (A := A) (B := B) (Γ := Δ) (L := L)).vwk (ρ.slift)
+  = inj_l := rfl
+
+@[simp]
+theorem Eqv.vsubst_lift_inj_l {A B : Ty α} {Γ Δ : Ctx α ε} {L : LCtx α}
+  {ρ : Term.Subst.Eqv φ Γ Δ}
+  : (inj_l (φ := φ) (A := A) (B := B) (Γ := Δ) (L := L)).vsubst (ρ.lift (le_refl _))
+  = inj_l := by induction ρ using Quotient.inductionOn; rfl
+
 theorem Eqv.lwk1_inj_l {A B : Ty α} {Γ : Ctx α ε} {L : LCtx α}
   : (inj_l (φ := φ) (A := A) (B := B) (Γ := Γ) (L := L)).lwk1 (inserted := inserted)
   = inj_l := rfl
@@ -135,10 +153,28 @@ def Eqv.inj_r {A B : Ty α} {Γ : Ctx α ε} {L : LCtx α}
 theorem Eqv.inj_r_eq_ret {A B : Ty α} {Γ : Ctx α ε} {L : LCtx α}
   : Eqv.inj_r (φ := φ) (A := A) (B := B) (Γ := Γ) (L := L) = ret Term.Eqv.inj_r := rfl
 
+@[simp]
 theorem Eqv.vwk1_inj_r {A B : Ty α} {Γ : Ctx α ε} {L : LCtx α}
   : (inj_r (φ := φ) (A := A) (B := B) (Γ := Γ) (L := L)).vwk1 (inserted := inserted)
   = inj_r := rfl
 
+@[simp]
+theorem Eqv.vwk2_inj_r {A B : Ty α} {Γ : Ctx α ε} {L : LCtx α}
+  : (inj_r (φ := φ) (A := A) (B := B) (Γ := V::Γ) (L := L)).vwk2 (inserted := inserted)
+  = inj_r := rfl
+
+@[simp]
+theorem Eqv.vwk_lift_inj_r {A B : Ty α} {Γ Δ : Ctx α ε} {L : LCtx α}
+  {ρ : Γ.InS Δ}
+  : (inj_r (φ := φ) (A := A) (B := B) (Γ := Δ) (L := L)).vwk (ρ.slift)
+  = inj_r := rfl
+
+@[simp]
+theorem Eqv.vsubst_lift_inj_r {A B : Ty α} {Γ Δ : Ctx α ε} {L : LCtx α}
+  {ρ : Term.Subst.Eqv φ Γ Δ}
+  : (inj_r (φ := φ) (A := A) (B := B) (Γ := Δ) (L := L)).vsubst (ρ.lift (le_refl _))
+  = inj_r := by induction ρ using Quotient.inductionOn; rfl
+
 theorem Eqv.lwk1_inj_r {A B : Ty α} {Γ : Ctx α ε} {L : LCtx α}
   : (inj_r (φ := φ) (A := A) (B := B) (Γ := Γ) (L := L)).lwk1 (inserted := inserted)
   = inj_r := rfl

DeBruijnSSA/BinSyntax/Rewrite/Region/Structural.lean

@@ -73,7 +73,7 @@ theorem Eqv.vwk_liftn₂_packed {Γ Δ Δ' : Ctx α ε} {R : LCtx α} {r : Eqv 
   simp [<-Ctx.InS.lift_lift]
 
 @[simp]
-theorem Eqv.vwk1_packed {Γ Δ : Ctx α ε} {R : LCtx α} {r : Eqv φ (V::Γ) R}
+theorem Eqv.vwk1_packed {Γ Δ : Ctx α ε} {R : LCtx α} {r : Eqv φ Γ R}
   : r.packed.vwk1 (inserted := inserted) = r.packed (Δ := _::Δ) := by
   rw [vwk1, <-Ctx.InS.lift_wk0, vwk_slift_packed]
 
@@ -161,6 +161,19 @@ theorem Eqv.packed_cfg_split {Γ : Ctx α ε} {L R : LCtx α} {β : Eqv φ Γ (R
   · rw [packed_in_unpacked_app_out, <-packed]
   · rw [packed_in_pack_coprod_arr]; congr; funext i; rw [packed_in_unpacked_app_out, <-packed]
 
+theorem Eqv.packed_cfg_split_vwk1 {Γ : Ctx α ε} {L R : LCtx α} {β : Eqv φ Γ (R ++ L)} {G}
+  : (cfg R β G).packed (Δ := Δ)
+  = letc (Γ.pack.prod R.pack)
+      (ret Term.Eqv.split ;; _ ⋊ β.packed.unpacked_app_out)
+      (ret Term.Eqv.split ⋉ _ ;; assoc
+        ;; _ ⋊ (ret Term.Eqv.distl_pack
+          ;; pack_coprod (λi => acast R.get_dist
+            ;; (G (i.cast R.length_dist)).packed.unpacked_app_out))).vwk1 := by
+  rw [packed_cfg_split]
+  simp only [List.get_eq_getElem, Fin.coe_cast, vwk1_seq, vwk1_ltimes, vwk1_br, wk1_split,
+    vwk1_rtimes, wk1_distl_pack, vwk1_pack_coprod, vwk1_acast, vwk1_unpacked_app_out, vwk1_packed]
+  rfl
+
 -- TODO: unpacked_app_out ltimes dinaturality
 
 end Region

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

@@ -8,17 +8,26 @@ variable [Φ: EffInstSet φ (Ty α) ε] [PartialOrder α] [SemilatticeSup ε] [O
 
 namespace Region
 
-def Eqv.fixpoint_def' {A B : Ty α} {Γ : Ctx α ε} {L : LCtx α} (f : Eqv φ (⟨A, ⊥⟩::Γ) ((B.coprod A)::L))
-  : Eqv φ (⟨A, ⊥⟩::Γ) (B::L) := letc A nil (f.vwk1.lwk1 ;; left_exit)
+def Eqv.fixpoint_def' {A B : Ty α} {Γ : Ctx α ε} {L : LCtx α}
+  {f : Eqv φ (⟨A, ⊥⟩::Γ) ((B.coprod A)::L)}
+  : fixpoint f = letc A nil (f.vwk1.lwk1 ;; left_exit)
+  := rfl
 
-theorem Eqv.letc_to_vwk1 {Γ : Ctx α ε} {L : LCtx α} {A : Ty α} {β : Eqv φ ((B, ⊥)::Γ) (A::L)} {G}
-  : letc A β G = letc (B.prod A)
-    (ret Term.Eqv.split ;; _ ⋊ β)
-    ((ret Term.Eqv.split ⋉ _ ;; assoc ;; _ ⋊ (let2 (Term.Eqv.var 0 Ctx.Var.shead) G.vwk2)).vwk1)
-  := by
-  sorry
+
+def Eqv.fixpoint_def_vwk1 {A B : Ty α} {Γ : Ctx α ε} {L : LCtx α}
+  {f : Eqv φ (⟨A, ⊥⟩::Γ) ((B.coprod A)::L)}
+  : fixpoint f = letc A nil (f.lwk1 ;; left_exit).vwk1
+  := by rw [vwk1_seq, vwk1_lwk1]; rfl
+
+-- theorem Eqv.letc_to_vwk1 {Γ : Ctx α ε} {L : LCtx α} {A : Ty α} {β : Eqv φ ((B, ⊥)::Γ) (A::L)} {G}
+--   : letc A β G = letc (B.prod A)
+--     (ret Term.Eqv.split ;; _ ⋊ β)
+--     ((ret Term.Eqv.split ⋉ _ ;; assoc ;; _ ⋊ (let2 (Term.Eqv.var 0 Ctx.Var.shead) G.vwk2)).vwk1)
+--   := by
+--   sorry
 
 theorem Eqv.letc_vwk1_den {Γ : Ctx α ε}
   {A B : Ty α} {β : Eqv φ ((X, ⊥)::Γ) [A, B]} {G : Eqv φ ((A, ⊥)::Γ) [A, B]}
-  : letc A β G.vwk1 = β.packed_out ;; fixpoint (coprod (coprod zero inj_l) (G.packed_out ;; inj_r))
+  : letc A β G.vwk1 = (β.packed_out ;; sum (coprod zero nil) nil) ;;
+                    coprod nil (fixpoint (G.packed_out ;; coprod (coprod zero inj_l) inj_r))
   := sorry

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

@@ -60,6 +60,10 @@ theorem Eqv.vwk2_packed_in {Γ Δ : Ctx α ε} {R : LCtx α} {r : Eqv φ Γ R}
   : r.packed_in.vwk2 (inserted := inserted) = r.packed_in (Δ := head::_::Δ) := by
   rw [vwk2, <-Ctx.InS.lift_wk1, vwk_slift_packed_in]
 
+theorem Eqv.lwk1_packed_in {Γ Δ : Ctx α ε} {R : LCtx α} {r : Eqv φ Γ (A::R)}
+  : r.packed_in.lwk1 (inserted := inserted) = r.lwk1.packed_in (Δ := Δ) := by
+  rw [packed_in, lwk1, packed_in, lwk1, vsubst_lwk]
+
 @[simp]
 theorem Eqv.vsubst_lift_packed_in {Γ Δ Δ' : Ctx α ε} {R : LCtx α} {r : Eqv φ Γ R}
   {σ : Term.Subst.Eqv φ Δ' Δ}

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

@@ -169,6 +169,19 @@ theorem Subst.Eqv.vliftn₂_unpack {Γ : Ctx α ε} {R : LCtx α}
   : (Subst.Eqv.unpack (φ := φ) (Γ := Γ) (R := R)).vliftn₂ (left := left) (right := right)
   = unpack := by simp [Subst.Eqv.vliftn₂_eq_vlift_vlift]
 
+@[simp]
+theorem Subst.Eqv.vwk_unpack {Γ : Ctx α ε} {R : LCtx α} {ρ : Γ.InS Δ}
+  : (Subst.Eqv.unpack (φ := φ) (R := R)).vwk ρ = unpack := by
+  rw [unpack_def, vwk_quot, unpack_def]
+  apply congrArg; ext; simp
+
+@[simp]
+theorem Subst.Eqv.vsubst_unpack {Γ Δ : Ctx α ε} {R : LCtx α} (σ : Term.Subst.Eqv φ Δ Γ)
+  : (Subst.Eqv.unpack (φ := φ) (R := R)).vsubst σ = unpack := by
+  induction σ using Quotient.inductionOn
+  rw [unpack_def, vsubst_quot, unpack_def]
+  apply congrArg; ext; simp
+
 def Subst.Eqv.pack {Γ : Ctx α ε} {R : LCtx α} : Subst.Eqv φ Γ R [R.pack] := ⟦Subst.InS.pack⟧
 
 @[simp]
@@ -243,7 +256,13 @@ theorem Eqv.unpacked_out_case {Γ : Ctx α ε} {R : LCtx α}
   (l : Eqv φ ((A, ⊥)::Γ) [R.pack]) (r : Eqv φ ((B, ⊥)::Γ) [R.pack])
   : (case a l r).unpacked_out = case a l.unpacked_out r.unpacked_out := by simp [unpacked_out]
 
--- TODO: unpacking a cfg is a quarter of Böhm–Jacopini
+theorem Eqv.vsubst_unpacked_out {Γ : Ctx α ε} {R : LCtx α} {σ : Term.Subst.Eqv φ Γ Δ}
+  {r : Eqv φ Δ [R.pack]} : r.unpacked_out.vsubst σ = (r.vsubst σ).unpacked_out := by
+  simp [unpacked_out, vsubst_lsubst]
+
+theorem Eqv.unpacked_out_vsubst {Γ : Ctx α ε} {R : LCtx α} {σ : Term.Subst.Eqv φ Γ Δ}
+  {r : Eqv φ Δ [R.pack]} : (r.vsubst σ).unpacked_out = r.unpacked_out.vsubst σ
+  := vsubst_unpacked_out.symm
 
 def Eqv.packed_out {Γ : Ctx α ε} {R : LCtx α} (h : Eqv φ Γ R) : Eqv φ Γ [R.pack]
   := h.lsubst Subst.Eqv.pack
@@ -556,6 +575,12 @@ theorem Eqv.vwk1_packed_out {Γ : Ctx α ε} {R : LCtx α} {r : Eqv φ (V::Γ) R
   rw [packed_out, packed_out, <-Subst.Eqv.vlift_pack, Subst.Eqv.vwk1_lsubst_vlift,
       Subst.Eqv.vlift_pack, Subst.Eqv.vlift_pack, <-packed_out]
 
+-- theorem Eqv.lwk1_packed_out {Γ : Ctx α ε} {R : LCtx α} {r : Eqv φ (V::Γ) R}
+--   : r.packed_out.lwk1 (inserted := inserted) = r.packed_out := by
+--   sorry
+  -- rw [packed_out, packed_out, <-Subst.Eqv.vlift_pack, Subst.Eqv.lwk1_lsubst_vlift,
+  --     Subst.Eqv.vlift_pack, Subst.Eqv.vlift_pack, <-packed_out]
+
 theorem Eqv.unpacked_app_out_let1 {Γ : Ctx α ε} {R L : LCtx α}
   {a : Term.Eqv φ Γ (A, e)} {r : Eqv φ ((A, ⊥)::Γ) [(R ++ L).pack]}
   : (let1 a r).unpacked_app_out = let1 a r.unpacked_app_out := by simp [unpacked_app_out]

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

@@ -21,6 +21,11 @@ theorem Eqv.wk1_distl_inv {A B C : Ty α} {Γ : Ctx α ε}
     (inserted := inserted)
   = distl_inv := rfl
 
+@[simp]
+theorem Eqv.wk_lift_distl_inv {A B C : Ty α} {Γ Δ : Ctx α ε} {ρ : Γ.InS Δ}
+  : (distl_inv (φ := φ) (A := A) (B := B) (C := C) (Γ := Δ) (e := e)).wk ρ.slift
+  = distl_inv := rfl
+
 theorem Eqv.seq_distl_inv_eq_let {X A B C : Ty α} {Γ : Ctx α ε}
   {r : Eqv φ ((X, ⊥)::Γ) ⟨A.prod (B.coprod C), e⟩}
   : r ;;' distl_inv = let1 r distl_inv

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

@@ -90,6 +90,14 @@ theorem Eqv.let2_nil {A B : Ty α} {Γ : Ctx α ε} (a : Eqv φ Γ ⟨A.prod B,
 def Eqv.split {A : Ty α} {Γ : Ctx α ε} : Eqv (φ := φ) (⟨A, ⊥⟩::Γ) ⟨A.prod A, e⟩
   := pair nil nil
 
+@[simp]
+theorem Eqv.wk_lift_split {A : Ty α} {Γ Δ : Ctx α ε} {ρ : Ctx.InS Γ Δ}
+  : split.wk ρ.slift = split (φ := φ) (A := A) (e := e) := rfl
+
+@[simp]
+theorem Eqv.wk1_split {A : Ty α} {Γ : Ctx α ε}
+  : (split (Γ := Γ)).wk1 (inserted := inserted) = split (φ := φ) (A := A) (e := e) := rfl
+
 theorem Eqv.pl_split {A : Ty α} {Γ : Ctx α ε}
   : split.pl = nil (φ := φ) (Γ := Γ) (A := A) (e := e)
   := by rw [pl, split, let2_pair, nil, let1_beta_var0, wk0_var, let1_beta_var1]; rfl

DeBruijnSSA/BinSyntax/Rewrite/Term/Structural/Distrib.lean

@@ -22,6 +22,19 @@ theorem Eqv.split_rtimes_pi_r_distl_packed {A B : Ty α} {Γ : Ctx α ε}
     (_ ⋊' (split ;;' inj_r ⋉' _) ;;' assoc_inv)
   := split_rtimes_pi_r_distl
 
+@[simp]
+theorem Eqv.wk_lift_distl_pack {Γ Δ : Ctx α ε} {ρ : Γ.InS Δ}
+  : (distl_pack (φ := φ) (R := R) (X := X) (e := e)).wk ρ.slift = distl_pack := by
+  induction R with
+  | nil => rfl
+  | cons A R I => simp [distl_pack, wk_lift_seq, wk_lift_coprod, I]
+
+@[simp]
+theorem Eqv.wk1_distl_pack {Γ : Ctx α ε} {R : LCtx α} {X : Ty α}
+  : (distl_pack (φ := φ) (Γ := Γ) (R := R) (X := X) (e := e)).wk1 (inserted := inserted)
+  = distl_pack
+  := by rw [wk1, <-Ctx.InS.lift_wk0, wk_lift_distl_pack]
+
 -- theorem Eqv.split_rtimes_nil_packed_distl {A B C : Ty α} {Γ : Ctx α ε}
 --   : split (φ := φ) (A := Ctx.pack ((A.coprod B, ⊥)::Γ)) (e := e) (Γ := Δ)
 --   ;;' _ ⋊' Term.Eqv.nil.packed ;;' distl_inv