Completeness theorem

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

@@ -1,8 +1,7 @@
-import DeBruijnSSA.BinSyntax.Rewrite.Region.LSubst
 import DeBruijnSSA.BinSyntax.Rewrite.Region.Compose.Seq
 import DeBruijnSSA.BinSyntax.Rewrite.Region.Compose.Product
 import DeBruijnSSA.BinSyntax.Rewrite.Region.Compose.Sum
-import DeBruijnSSA.BinSyntax.Typing.Region.Compose
+import DeBruijnSSA.BinSyntax.Rewrite.Term.Compose.Distrib
 
 namespace BinSyntax
 
@@ -56,15 +55,34 @@ theorem Eqv.let2_eta_seq_distl_inv {A B C : Ty α} {Γ : Ctx α ε} {L : LCtx α
   ]
   rfl
 
+theorem Eqv.distl_eq_ret {A B C : Ty α} {Γ : Ctx α ε} {L : LCtx α}
+  : distl (φ := φ) (A := A) (B := B) (C := C) (Γ := Γ) (L := L)
+  = ret Term.Eqv.distl := by
+  simp only [Term.Eqv.distl, ret_of_coprod, <-rtimes_eq_ret]
+  rfl
+
+theorem Eqv.distl_inv_eq_ret {A B C : Ty α} {Γ : Ctx α ε} {L : LCtx α}
+  : distl_inv (φ := φ) (A := A) (B := B) (C := C) (Γ := Γ) (L := L)
+  = ret Term.Eqv.distl_inv := by
+  simp only [Term.Eqv.distl_inv, <-let2_ret, ret_of_coprod]; rfl
+
 theorem Eqv.Pure.distl {A B C : Ty α} {Γ : Ctx α ε} {L : LCtx α}
-  : (distl (φ := φ) (A := A) (B := B) (C := C) (Γ := Γ) (L := L)).Pure := sorry
+  : (distl (φ := φ) (A := A) (B := B) (C := C) (Γ := Γ) (L := L)).Pure
+  := ⟨Term.Eqv.distl, distl_eq_ret⟩
 
 theorem Eqv.Pure.distl_inv {A B C : Ty α} {Γ : Ctx α ε} {L : LCtx α}
-  : (distl_inv (φ := φ) (A := A) (B := B) (C := C) (Γ := Γ) (L := L)).Pure := sorry
+  : (distl_inv (φ := φ) (A := A) (B := B) (C := C) (Γ := Γ) (L := L)).Pure
+  := ⟨Term.Eqv.distl_inv, distl_inv_eq_ret⟩
 
--- TODO: dist isomorphism
+theorem Eqv.distl_distl_inv {A B C : Ty α} {Γ : Ctx α ε} {L : LCtx α}
+  : distl (φ := φ) (A := A) (B := B) (C := C) (Γ := Γ) (L := L)
+  ;; distl_inv = nil := by
+  rw [distl_eq_ret, distl_inv_eq_ret, <-ret_of_seq, Term.Eqv.distl_distl_inv_pure]; rfl
 
--- TODO: "naturality"
+theorem Eqv.distl_inv_distl {A B C : Ty α} {Γ : Ctx α ε} {L : LCtx α}
+  : distl_inv (φ := φ) (A := A) (B := B) (C := C) (Γ := Γ) (L := L)
+  ;; distl = nil := by
+  rw [distl_eq_ret, distl_inv_eq_ret, <-ret_of_seq, Term.Eqv.distl_inv_distl_pure]; rfl
 
 def Eqv.left_exit {A B : Ty α} {Γ : Ctx α ε} {L : LCtx α}
   : Eqv φ (⟨A.coprod B, ⊥⟩::Γ) (B::A::L) :=

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

@@ -577,6 +577,45 @@ theorem Eqv.assoc_mid_nat {A B C B' : Ty α} {Γ : Ctx α ε} {L : LCtx α}
     congr
     funext k; cases k <;> rfl
 
+theorem Eqv.seq_let2_wk0_pure {Γ : Ctx α ε} {L : LCtx α}
+  {a : Term.Eqv φ Γ ⟨X.prod Y, ⊥⟩}
+  {r : Eqv φ (⟨A, ⊥⟩::Γ) (B::L)} {s : Eqv φ (⟨Y, ⊥⟩::⟨X, ⊥⟩::⟨B, ⊥⟩::Γ) (C::L)}
+  : r ;; (let2 a.wk0 s) = let2 a.wk0 (r.vwk1.vwk1 ;; s.vswap02.vswap02).vswap02 := by
+  rw [
+    <-Term.Eqv.pair_eta_pure (p := a.wk0), let2_pair, <-Term.Eqv.wk0_pl,
+    seq_let1_wk0_pure, <-Term.Eqv.wk0_pr, <-Term.Eqv.pair_eta_pure (p := a.wk0),
+    let2_pair, wk0_pl
+  ]
+  apply congrArg
+  conv => lhs; rhs; rhs; rw [vswap01, vwk_let1, <-Term.Eqv.swap01_def, Term.Eqv.swap01_wk0_wk0]
+  rw [seq_let1_wk0_pure]
+  simp only [vswap01, vwk_let1, vswap02]
+  rw [<-Term.Eqv.swap01_def, Term.Eqv.swap01_wk0_wk0, <-Term.Eqv.wk0_pr]
+  apply congrArg
+  induction r using Quotient.inductionOn
+  induction s using Quotient.inductionOn
+  apply Eqv.eq_of_reg_eq
+  simp only [Set.mem_setOf_eq, InS.coe_vwk, Ctx.InS.coe_lift, Ctx.InS.coe_swap01, InS.coe_lsubst,
+    InS.coe_alpha0, Ctx.InS.coe_wk1, vwk_lsubst, Ctx.InS.coe_swap02]
+  congr 1
+  · funext k
+    cases k with
+    | zero =>
+      simp only [alpha, Region.vwk_vwk, Function.comp_apply, Function.update_same]
+      congr
+      funext k; cases k using Nat.cases3 <;> rfl
+    | succ => rfl
+  · simp only [Region.vwk_vwk]
+    congr
+    funext k; cases k <;> rfl
+
+theorem Eqv.seq_let2_wk0_pure' {Γ : Ctx α ε} {L : LCtx α}
+  {a : Term.Eqv φ (_::Γ) ⟨X.prod Y, ⊥⟩} {a' : Term.Eqv φ Γ ⟨X.prod Y, ⊥⟩}
+  {r : Eqv φ (⟨A, ⊥⟩::Γ) (B::L)} {s : Eqv φ (⟨Y, ⊥⟩::⟨X, ⊥⟩::⟨B, ⊥⟩::Γ) (C::L)}
+  (ha : a = a'.wk0)
+  : r ;; (let2 a s) = let2 a'.wk0 (r.vwk1.vwk1 ;; s.vswap02.vswap02).vswap02 := by
+  cases ha; rw [seq_let2_wk0_pure]
+
 theorem Eqv.assoc_right_nat {A B C C' : Ty α} {Γ : Ctx α ε} {L : LCtx α}
   (r : Eqv φ (⟨C, ⊥⟩::Γ) (C'::L))
   : (A.prod B) ⋊ r ;; assoc = assoc ;; A ⋊ (B ⋊ r) := by

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

@@ -225,67 +225,6 @@ theorem Eqv.seq_let1_wk0_pure {Γ : Ctx α ε} {L : LCtx α}
   · rw [Region.vwk_vwk, <-Region.vsubst_fromWk, Region.vsubst_vsubst, Region.vsubst_id']
     funext k; cases k <;> rfl
 
--- theorem Eqv.lsubst_let2_alpha0 {Γ : Ctx α ε} {L : LCtx α}
---   (p : Term.Eqv φ Γ ⟨X.prod Y, ⊥⟩)
---   (r : Eqv φ (⟨A, ⊥⟩::Γ) (B::L)) (s : Eqv φ (⟨Y, ⊥⟩::⟨X, ⊥⟩::⟨B, ⊥⟩::⟨A, ⊥⟩::Γ) (C::L))
---   : lsubst (let2 p.wk0.wk0 s).alpha0 r
---   = let2 p.wk0 (lsubst (alpha0 s.vswap02.vswap02) r.vwk0.vwk0)
---   := by induction r using Eqv.arrow_induction with
---   | br ℓ a hℓ =>
---     cases ℓ with
---     | zero =>
---       induction p using Quotient.inductionOn
---       induction s using Quotient.inductionOn
---       induction a using Quotient.inductionOn
---       apply Eqv.eq_of_reg_eq
---       simp only [Set.mem_setOf_eq, InS.lsubst_br, List.length_cons, List.get_eq_getElem,
---         InS.coe_vsubst, Term.InS.coe_subst0, InS.coe_vwk_id, Subst.InS.coe_get, InS.coe_alpha0,
---         InS.coe_let2, Term.InS.coe_wk, Ctx.InS.coe_wk0, InS.vwk_br, InS.coe_vwk, Ctx.InS.coe_swap02]
---       simp only [Region.vsubst, Term.wk_succ_subst_subst0, alpha, ← vsubst_fromWk,
---         Region.vsubst_vsubst, Function.update_same, let2.injEq, true_and]
---       congr
---       funext k; cases k using Nat.cases3 with
---       | two => simp only [Term.Subst.liftn, lt_self_iff_false, ↓reduceIte, le_refl,
---         tsub_eq_zero_of_le, Term.subst0_zero, Term.Subst.comp, Term.subst, Term.wk_wk,
---         Nat.one_lt_ofNat, Nat.swap0_lt, Nat.ofNat_pos]; rfl
---       | _ => rfl
---     | succ ℓ => simp [get_alpha0, let2_br, Term.Eqv.nil, Term.Eqv.let2_wk0_wk0_pure]
---   | let1 a r => sorry
---   | let2 a r => sorry
---   | case a l r => sorry
---   | cfg R β G => sorry
-
-theorem Eqv.seq_let2_wk0_pure {Γ : Ctx α ε} {L : LCtx α}
-  {a : Term.Eqv φ Γ ⟨X.prod Y, ⊥⟩}
-  {r : Eqv φ (⟨A, ⊥⟩::Γ) (B::L)} {s : Eqv φ (⟨Y, ⊥⟩::⟨X, ⊥⟩::⟨B, ⊥⟩::Γ) (C::L)}
-  : r ;; (let2 a.wk0 s) = let2 a.wk0 (r.vwk1.vwk1 ;; s.vswap02.vswap02).vswap02 := by
-  sorry
-  -- rw [seq, vwk1_let2, Term.Eqv.wk0_wk1, lsubst_let2_alpha0]
-  -- congr
-  -- rw [seq]
-  -- induction r using Quotient.inductionOn
-  -- induction s using Quotient.inductionOn
-  -- induction a using Quotient.inductionOn
-  -- apply Eqv.eq_of_reg_eq
-  -- simp only [Set.mem_setOf_eq, InS.coe_lsubst, InS.coe_alpha0, InS.coe_vwk, Ctx.InS.coe_swap02,
-  --   Ctx.InS.coe_wk3, Ctx.InS.coe_wk0, Ctx.InS.coe_wk1, vwk_lsubst]
-  -- congr 1
-  -- · funext k; cases k with
-  --   | zero =>
-  --     simp only [alpha, Region.vwk_vwk, Function.update_same, Function.comp_apply]
-  --     congr
-  --     funext k; cases k using Nat.cases3 <;> rfl
-  --   | succ => rfl
-  -- · simp only [Region.vwk_vwk]; congr; funext k; cases k <;> rfl
-
-theorem Eqv.seq_let2_wk0_pure' {Γ : Ctx α ε} {L : LCtx α}
-  {a : Term.Eqv φ (_::Γ) ⟨X.prod Y, ⊥⟩} {a' : Term.Eqv φ Γ ⟨X.prod Y, ⊥⟩}
-  {r : Eqv φ (⟨A, ⊥⟩::Γ) (B::L)} {s : Eqv φ (⟨Y, ⊥⟩::⟨X, ⊥⟩::⟨B, ⊥⟩::Γ) (C::L)}
-  (ha : a = a'.wk0)
-  : r ;; (let2 a s) = let2 a'.wk0 (r.vwk1.vwk1 ;; s.vswap02.vswap02).vswap02 := by
-  cases ha; rw [seq_let2_wk0_pure]
-
-
 theorem Eqv.case_seq {Γ : Ctx α ε} {L : LCtx α}
   (a : Term.Eqv φ (⟨A, ⊥⟩::Γ) ⟨X.coprod Y, e⟩)
   (r : Eqv φ (⟨X, ⊥⟩::⟨A, ⊥⟩::Γ) (B::L)) (s : Eqv φ (⟨Y, ⊥⟩::⟨A, ⊥⟩::Γ) (B::L))

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

@@ -106,40 +106,40 @@ theorem Subst.Eqv.unpack_comp_pack {Γ : Ctx α ε} {R : LCtx α}
   : Subst.Eqv.unpack.comp Subst.Eqv.pack = Subst.Eqv.id (φ := φ) (Γ := Γ) (L := R)
   := by ext ℓ; simp [get_comp, pack_get, get_id, unpack, Eqv.csubst_get, Eqv.vsubst0_pack_unpack]
 
-theorem Eqv.lsubst_pack_unpack {Γ : Ctx α ε} {R : LCtx α}
-  : (unpack (φ := φ) (Γ := Γ) (R := R)).lsubst Subst.Eqv.pack
-  = nil := by
-  induction R with
-  | nil =>
-    apply Eqv.initial
-    sorry -- TODO: context containing empty is trivially initial, add simp lemmas...
-  | cons A R I =>
-    simp only [LCtx.pack.eq_2, unpack, coprod, vwk1_quot, InS.nil_vwk1, vwk1_lwk0, vwk1_unpack,
-      lsubst_case, Subst.Eqv.vlift_pack]
-    apply Eq.trans _ Eqv.sum_nil
-    simp only [sum, coprod]
-    congr
-    -- TODO: lsubst pack lwk0 is lsubst pack ;; inj_r; then follows by induction
-    sorry
-
-theorem Subst.Eqv.pack_comp_unpack {Γ : Ctx α ε} {R : LCtx α}
-  : Subst.Eqv.pack.comp Subst.Eqv.unpack = Subst.Eqv.id (φ := φ) (Γ := Γ) (L := [R.pack]) := by
-  ext ℓ
-  induction ℓ using Fin.elim1
-  simp only [unpack, get_comp, vlift_pack, Eqv.csubst_get, Eqv.cast_rfl, Eqv.lsubst_pack_unpack,
-    get_id, Fin.coe_fin_one]
-  rfl
+-- theorem Eqv.lsubst_pack_unpack {Γ : Ctx α ε} {R : LCtx α}
+--   : (unpack (φ := φ) (Γ := Γ) (R := R)).lsubst Subst.Eqv.pack
+--   = nil := by
+--   induction R with
+--   | nil =>
+--     apply Eqv.initial
+--     sorry -- TODO: context containing empty is trivially initial, add simp lemmas...
+--   | cons A R I =>
+--     simp only [LCtx.pack.eq_2, unpack, coprod, vwk1_quot, InS.nil_vwk1, vwk1_lwk0, vwk1_unpack,
+--       lsubst_case, Subst.Eqv.vlift_pack]
+--     apply Eq.trans _ Eqv.sum_nil
+--     simp only [sum, coprod]
+--     congr
+--     -- TODO: lsubst pack lwk0 is lsubst pack ;; inj_r; then follows by induction
+--     sorry
+
+-- theorem Subst.Eqv.pack_comp_unpack {Γ : Ctx α ε} {R : LCtx α}
+--   : Subst.Eqv.pack.comp Subst.Eqv.unpack = Subst.Eqv.id (φ := φ) (Γ := Γ) (L := [R.pack]) := by
+--   ext ℓ
+--   induction ℓ using Fin.elim1
+--   simp only [unpack, get_comp, vlift_pack, Eqv.csubst_get, Eqv.cast_rfl, Eqv.lsubst_pack_unpack,
+--     get_id, Fin.coe_fin_one]
+--   rfl
 
 def Eqv.unpacked {Γ : Ctx α ε} {R : LCtx α} (h : Eqv φ Γ [R.pack]) : Eqv φ Γ R
   := h.lsubst Subst.Eqv.unpack
 
 def Eqv.packed {Γ : Ctx α ε} {R : LCtx α} (h : Eqv φ Γ R) : Eqv φ Γ [R.pack]
   := h.lsubst Subst.Eqv.pack
 
-theorem Eqv.unpacked_packed {Γ : Ctx α ε} {R : LCtx α} (h : Eqv φ Γ R)
-  : h.packed.unpacked = h := by
-  rw [Eqv.unpacked, packed, lsubst_lsubst, Subst.Eqv.unpack_comp_pack]
-  sorry
+-- theorem Eqv.unpacked_packed {Γ : Ctx α ε} {R : LCtx α} (h : Eqv φ Γ R)
+--   : h.packed.unpacked = h := by
+--   rw [Eqv.unpacked, packed, lsubst_lsubst, Subst.Eqv.unpack_comp_pack]
+--   sorry
 
 end Region
 

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

@@ -0,0 +1,77 @@
+import DeBruijnSSA.BinSyntax.Rewrite.Term.Compose.Sum
+import DeBruijnSSA.BinSyntax.Rewrite.Term.Compose.Product
+
+namespace BinSyntax
+
+variable [Φ: EffInstSet φ (Ty α) ε] [PartialOrder α] [SemilatticeSup ε] [OrderBot ε]
+
+namespace Term
+
+def Eqv.distl {A B C : Ty α} {Γ : Ctx α ε}
+  : Eqv φ (⟨(A.prod B).coprod (A.prod C), ⊥⟩::Γ) ⟨A.prod (B.coprod C), e⟩
+  := coprod (A ⋊' inj_l) (A ⋊' inj_r)
+
+def Eqv.distl_inv {A B C : Ty α} {Γ : Ctx α ε}
+  : Eqv φ (⟨A.prod (B.coprod C), ⊥⟩::Γ) ⟨(A.prod B).coprod (A.prod C), e⟩
+  := let2 nil (coprod (inl (pair (var 1 (by simp)) nil)) (inr (pair (var 1 (by simp)) nil)))
+
+theorem Eqv.distl_distl_inv_pure {A B C : Ty α} {Γ : Ctx α ε}
+  : (distl : Eqv φ (⟨(A.prod B).coprod (A.prod C), ⊥⟩::Γ) ⟨A.prod (B.coprod C), ⊥⟩)
+  ;;' distl_inv = nil := by
+  simp only [distl, distl_inv, coprod_seq]
+  simp [
+    seq, let1_beta_pure, coprod, wk1_let2, rtimes, wk1_tensor, let2_tensor, subst_liftn₂_tensor,
+    wk2, Nat.liftnWk, nil, inj_l, inj_r, case_inl, case_inr, <-inl_let2, <-inr_let2, let2_eta,
+    case_eta
+  ]
+
+theorem Eqv.distl_inv_distl_pure {A B C : Ty α} {Γ : Ctx α ε}
+  : (distl_inv : Eqv φ (⟨A.prod (B.coprod C), ⊥⟩::Γ) ⟨(A.prod B).coprod (A.prod C), ⊥⟩)
+  ;;' distl = nil := by
+  simp only [distl_inv, distl, seq_let2, wk1_coprod, wk1_rtimes, wk1_inj_l, wk1_inj_r, coprod_seq,
+    inl_coprod, seq_rtimes, inr_coprod]
+  convert let2_eta
+  simp only [coprod, nil, wk1, inj_l, let2_pair, wk0_var, zero_add, wk_let1, wk_var,
+    Set.mem_setOf_eq, Ctx.InS.coe_wk1, Nat.liftWk_succ, Nat.succ_eq_add_one, Nat.reduceAdd,
+    Ctx.InS.lift_wk1, Ctx.InS.coe_wk2, Nat.liftnWk, Nat.one_lt_ofNat, ↓reduceIte, wk_pair,
+    Ctx.InS.coe_lift, zero_lt_two, wk_inl, Nat.liftWk_zero, inj_r, wk_inr]
+  calc
+    _ = let1
+      (case (var 0 Ctx.Var.shead) (var 0 Ctx.Var.shead).inl (var 0 Ctx.Var.shead).inr)
+      (pair (var 2 (by simp)) (var 0 Ctx.Var.shead)) := by
+      simp only [let1_case, wk1_pair, wk1_var_succ, Nat.reduceAdd, wk1_var0, List.length_cons,
+        Fin.zero_eta, List.get_eq_getElem, Fin.val_zero, List.getElem_cons_zero]
+      congr 1 <;> simp [let1_beta_pure]
+    _ = _ := by simp [case_eta, let1_beta_var0]
+
+theorem Eqv.wk_eff_distl {A B C : Ty α} {Γ : Ctx α ε} {h : lo ≤ hi}
+  : (distl : Eqv φ (⟨(A.prod B).coprod (A.prod C), ⊥⟩::Γ) ⟨A.prod (B.coprod C), _⟩).wk_eff h
+  = distl
+  := rfl
+
+theorem Eqv.wk_eff_distl_inv {A B C : Ty α} {Γ : Ctx α ε} {h : lo ≤ hi}
+  : (distl_inv : Eqv φ (⟨A.prod (B.coprod C), ⊥⟩::Γ) ⟨(A.prod B).coprod (A.prod C), _⟩).wk_eff h
+  = distl_inv
+  := rfl
+
+theorem Eqv.Pure.distl {A B C : Ty α} {Γ : Ctx α ε}
+  : (distl : Eqv φ (⟨(A.prod B).coprod (A.prod C), ⊥⟩::Γ) ⟨A.prod (B.coprod C), ⊥⟩).Pure
+  := ⟨Eqv.distl, rfl⟩
+
+theorem Eqv.Pure.distl_inv {A B C : Ty α} {Γ : Ctx α ε}
+  : (distl_inv : Eqv φ (⟨A.prod (B.coprod C), ⊥⟩::Γ) ⟨(A.prod B).coprod (A.prod C), ⊥⟩).Pure
+  := ⟨Eqv.distl_inv, rfl⟩
+
+theorem Eqv.distl_distl_inv {A B C : Ty α} {Γ : Ctx α ε}
+  : (distl : Eqv φ (⟨(A.prod B).coprod (A.prod C), ⊥⟩::Γ) ⟨A.prod (B.coprod C), e⟩)
+  ;;' distl_inv = nil := by rw [
+    <-wk_eff_distl (h := bot_le), <-wk_eff_distl_inv (h := bot_le), <-wk_eff_seq,
+    distl_distl_inv_pure, wk_eff_nil
+  ]
+
+theorem Eqv.distl_inv_distl {A B C : Ty α} {Γ : Ctx α ε}
+  : (distl_inv : Eqv φ (⟨A.prod (B.coprod C), ⊥⟩::Γ) ⟨(A.prod B).coprod (A.prod C), e⟩)
+  ;;' distl = nil := by rw [
+    <-wk_eff_distl (h := bot_le), <-wk_eff_distl_inv (h := bot_le), <-wk_eff_seq,
+    distl_inv_distl_pure, wk_eff_nil
+  ]

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

@@ -30,9 +30,38 @@ theorem Eqv.wk1_pl {A B : Ty α} {Γ : Ctx α ε}
   {a : Eqv φ (head::Γ) ⟨A.prod B, e⟩}
   : (a.pl).wk1 (inserted := inserted) = a.wk1.pl := by rw [wk1, wk_pl]; rfl
 
+theorem Eqv.wk2_pl {A B : Ty α} {Γ : Ctx α ε}
+  {a : Eqv φ (left::right::Γ) ⟨A.prod B, e⟩}
+  : (a.pl).wk2 (inserted := inserted) = a.wk2.pl := by rw [wk2, wk_pl]; rfl
+
+theorem Eqv.wk3_pl {A B : Ty α} {Γ : Ctx α ε}
+  {a : Eqv φ (left::mid::right::Γ) ⟨A.prod B, e⟩}
+  : (a.pl).wk3 (inserted := inserted) = a.wk3.pl := by rw [wk3, wk_pl]; rfl
+
 def Eqv.pr {A B : Ty α} {Γ : Ctx α ε} (a : Eqv φ Γ ⟨A.prod B, e⟩) : Eqv φ Γ ⟨B, e⟩
   := let2 a (var 0 (by simp))
 
+theorem Eqv.wk_pr {A B : Ty α} {Γ : Ctx α ε} {ρ : Ctx.InS Γ Δ}
+  {a : Eqv φ Δ ⟨A.prod B, e⟩}
+  : (a.pr).wk ρ = (a.wk ρ).pr := by
+  induction a using Quotient.inductionOn; rfl
+
+theorem Eqv.wk0_pr {A B : Ty α} {Γ : Ctx α ε}
+  {a : Eqv φ Γ ⟨A.prod B, e⟩}
+  : (a.pr).wk0 (head := head) = a.wk0.pr := by rw [wk0, wk_pr]; rfl
+
+theorem Eqv.wk1_pr {A B : Ty α} {Γ : Ctx α ε}
+  {a : Eqv φ (head::Γ) ⟨A.prod B, e⟩}
+  : (a.pr).wk1 (inserted := inserted) = a.wk1.pr := by rw [wk1, wk_pr]; rfl
+
+theorem Eqv.wk2_pr {A B : Ty α} {Γ : Ctx α ε}
+  {a : Eqv φ (left::right::Γ) ⟨A.prod B, e⟩}
+  : (a.pr).wk2 (inserted := inserted) = a.wk2.pr := by rw [wk2, wk_pr]; rfl
+
+theorem Eqv.wk3_pr {A B : Ty α} {Γ : Ctx α ε}
+  {a : Eqv φ (left::mid::right::Γ) ⟨A.prod B, e⟩}
+  : (a.pr).wk3 (inserted := inserted) = a.wk3.pr := by rw [wk3, wk_pr]; rfl
+
 theorem Eqv.let2_nil {A B : Ty α} {Γ : Ctx α ε} (a : Eqv φ Γ ⟨A.prod B, e⟩)
   : let2 a nil = a.pr := rfl
 
@@ -565,6 +594,12 @@ theorem Eqv.subst_lift_tensor {A A' B B' : Ty α} {Δ : Ctx α ε} {σ : Subst.E
       Term.subst_fromWk]
     rfl
 
+theorem Eqv.subst_liftn₂_tensor {A A' B B' : Ty α} {Δ : Ctx α ε} {σ : Subst.Eqv φ Γ Δ}
+  {l : Eqv φ (⟨A, ⊥⟩::V::Δ) ⟨A', e⟩} {r : Eqv φ (⟨B, ⊥⟩::V::Δ) ⟨B', e⟩}
+  : (tensor l r).subst (σ.liftn₂ (le_refl _) (le_refl _))
+  = tensor (l.subst (σ.liftn₂ (le_refl _) (le_refl _))) (r.subst (σ.liftn₂ (le_refl _) (le_refl _)))
+  := by simp only [←Subst.Eqv.lift_lift, subst_lift_tensor]
+
 def Eqv.ltimes {A A' : Ty α} {Γ : Ctx α ε} (l : Eqv φ (⟨A, ⊥⟩::Γ) ⟨A', e⟩) (B)
   : Eqv φ (⟨A.prod B, ⊥⟩::Γ) ⟨A'.prod B, e⟩ := tensor l nil
 
@@ -1166,3 +1201,15 @@ theorem Eqv.hexagon {X Y Z : Ty α} {Γ : Ctx α ε}
     Ctx.InS.coe_wk1, id_eq, subst_lift_braid, Nat.one_lt_ofNat, ↓dreduceIte]
   rw [let1_beta' (a' := (var 1 (by simp)).pair (var 2 (by simp))) (by rfl)]
   simp [braid, let2_pair, let1_beta_var1, let1_beta_var2]
+
+theorem Eqv.pair_pi_l_pi_r {A B : Ty α} {Γ : Ctx α ε}
+  : pair pi_l pi_r = nil (φ := φ) (Γ := Γ) (A := A.prod B) (e := e)
+  := Eqv.pair_pi_l_pi_r'_wk_eff (a := nil)
+
+theorem Eqv.Pure.pair_eta {A B : Ty α} {Γ : Ctx α ε} {p : Eqv φ Γ ⟨A.prod B, e⟩}
+  : p.Pure → pair p.pl p.pr = p
+  := Eqv.Pure.pair_pi_l_pi_r'
+
+theorem Eqv.pair_eta_pure {A B : Ty α} {Γ : Ctx α ε} {p : Eqv φ Γ ⟨A.prod B, ⊥⟩}
+  : pair p.pl p.pr = p
+  := Eqv.Pure.pair_eta (by simp)

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

@@ -63,6 +63,16 @@ theorem Eqv.nil_subst0 {Γ : Ctx α ε} (a : Eqv φ Γ ⟨A, ⊥⟩)
   : (nil (e := e)).subst a.subst0 = a.wk_eff bot_le
   := by induction a using Quotient.inductionOn; rfl
 
+@[simp]
+theorem Eqv.nil_subst_lift {Γ : Ctx α ε} {σ : Subst.Eqv φ Γ Δ}
+  : (nil : Eqv φ (⟨A, ⊥⟩::Δ) ⟨A, e⟩).subst (σ.lift (le_refl _)) = nil := by
+  induction σ using Quotient.inductionOn; rfl
+
+@[simp]
+theorem Eqv.nil_subst_liftn₂ {Γ : Ctx α ε} {σ : Subst.Eqv φ Γ Δ}
+  : (nil : Eqv φ (⟨A, ⊥⟩::⟨B, ⊥⟩::Δ) ⟨A, e⟩).subst (σ.liftn₂ (le_refl _) (le_refl _)) = nil := by
+  induction σ using Quotient.inductionOn; rfl
+
 @[simp]
 theorem Eqv.Pure.nil {A : Ty α} {Γ : Ctx α ε} : (nil (φ := φ) (A := A) (Γ := Γ) (e := e)).Pure
   := ⟨Eqv.nil, rfl⟩