Product tap... needs serious cleaning

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

@@ -56,6 +56,11 @@ theorem Eqv.braid_eq_ret {left right : Ty α} {Γ : Ctx α ε} {L : LCtx α}
   simp only [Eqv.braid, let2_ret]
   rfl
 
+@[simp]
+theorem Eqv.vwk1_braid {left right : Ty α} {Γ : Ctx α ε} {L : LCtx α} :
+  (Eqv.braid (φ := φ) (left := left) (right := right) (Γ := Γ) (L := L)).vwk1 (inserted := inserted)
+  = Eqv.braid := rfl
+
 theorem Eqv.Pure.braid {left right : Ty α} {Γ : Ctx α ε} {L : LCtx α}
   : Eqv.Pure (Eqv.braid (φ := φ) (left := left) (right := right) (Γ := Γ) (L := L))
   := ⟨_, braid_eq_ret⟩
@@ -91,17 +96,22 @@ theorem Eqv.rtimes_rtimes {A B C : Ty α} {Γ : Ctx α ε} {L : LCtx α}
   congr 1
   simp only [vwk1_rtimes, seq_assoc, vwk1_seq, ret_seq]
   congr 1
-  sorry
-  -- simp only [
-  --   vwk1, vwk_let2, wk_var, Nat.liftWk, vsubst_let2, vwk_vwk, Ctx.InS.liftn₂_comp_liftn₂,
-  --   subst_pair, subst_var, Term.Subst.InS.get_0_subst0, let2_pair, let1_beta,
-  --   vsubst_vsubst
-  -- ]
-  -- apply congrArg
-  -- rw [vwk1_seq, vwk1_seq, seq_assoc]
-  -- congr 1
-  -- · simp [vwk1, vwk_vwk]
-  -- · sorry
+  simp [rtimes, vsubst_let2, let2_pair, let1_beta, vsubst_vsubst]
+  induction r using Quotient.inductionOn
+  induction s using Quotient.inductionOn
+  apply Eqv.eq_of_reg_eq
+  simp only [Set.mem_setOf_eq, InS.vwk_br, Term.InS.wk_pair, Term.InS.wk_var, Ctx.InS.coe_wk1,
+    Nat.liftWk_succ, Nat.succ_eq_add_one, zero_add, Nat.reduceAdd, Nat.liftWk_zero, InS.coe_lsubst,
+    InS.coe_alpha0, InS.coe_br, Term.InS.coe_pair, Term.InS.coe_var, InS.coe_vwk, Region.vwk_vwk,
+    InS.coe_vsubst, Term.Subst.InS.coe_comp, Term.InS.coe_subst0, Term.Subst.InS.coe_liftn₂,
+    Region.vsubst_lsubst]
+  congr
+  · funext k
+    cases k <;> rfl
+  · simp only [<-Region.vsubst_fromWk, Region.vsubst_vsubst]
+    congr
+    funext k
+    cases k <;> rfl
 
 -- TODO: proper ltimes?
 def Eqv.ltimes {tyIn tyOut : Ty α} {Γ : Ctx α ε} {L : LCtx α}
@@ -176,7 +186,7 @@ theorem Eqv.vwk1_pi_l {Γ : Ctx α ε} {L : LCtx α}
 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
-  := sorry
+  := by simp [ret, pi_l, ret_seq, vwk1, vwk_ret, Nat.liftnWk, let2_pair, let1_beta]
 
 @[simp]
 theorem Eqv.Pure.pi_l {Γ : Ctx α ε} {L : LCtx α}
@@ -226,7 +236,14 @@ theorem Eqv.vwk1_pi_r {Γ : Ctx α ε} {L : LCtx α}
 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
-  := sorry
+  := by
+  simp only [pi_r, ret_seq, vwk1, vwk_let2, wk_var, Set.mem_setOf_eq, Ctx.InS.coe_wk1,
+    Nat.liftWk_zero, vwk_ret, Ctx.InS.coe_liftn₂, Nat.liftnWk, Nat.ofNat_pos, ↓reduceIte,
+    vsubst_let2, var0_subst0, List.length_cons, id_eq, Fin.zero_eta, List.get_eq_getElem,
+    Fin.val_zero, List.getElem_cons_zero, wk_res_self, vsubst_br, ge_iff_le, le_refl,
+    subst_liftn₂_var_zero, let2_pair, let1_beta, ret]
+  congr
+  exact subst0_wk0
 
 @[simp]
 theorem Eqv.Pure.pi_r {Γ : Ctx α ε} {L : LCtx α}
@@ -243,23 +260,42 @@ theorem Eqv.lunit_pi_r {ty : Ty α} {Γ : Ctx α ε} {L : LCtx α}
   : lunit (φ := φ) (ty := ty) (Γ := Γ) (L := L) ;; pi_r = nil
   := by simp only [pi_r_eq_ret, lunit_eq_ret, ret_ret, Term.Eqv.lunit_pi_r, ret_nil]
 
+theorem Eqv.ret_pair_braid {Γ : Ctx α ε} {L : LCtx α} {A B : Ty α}
+  {a : Term.Eqv φ ((X, ⊥)::Γ) (A, ⊥)} {b : Term.Eqv φ ((X, ⊥)::Γ) (B, ⊥)}
+  : ret (targets := L) (a.pair b) ;; braid = ret (pair b a) := by
+  simp only [braid, ret_seq, vwk1, vwk_let2, wk_var, Set.mem_setOf_eq, Ctx.InS.coe_wk1,
+    Nat.liftWk_zero, vwk_ret, wk_pair, Ctx.InS.coe_liftn₂, Nat.liftnWk, Nat.ofNat_pos, ↓reduceIte,
+    Nat.one_lt_ofNat, vsubst_let2, var0_subst0, List.length_cons, id_eq, Fin.zero_eta,
+    List.get_eq_getElem, Fin.val_zero, List.getElem_cons_zero, wk_res_self, vsubst_br, subst_pair,
+    ge_iff_le, le_refl, subst_liftn₂_var_zero, subst_liftn₂_var_one, let2_pair, let1_beta,
+    var_succ_subst0, ↓dreduceIte, Nat.reduceSub, Nat.reduceAdd]
+  simp only [ret]
+  congr
+  exact subst0_wk0
+
 theorem Eqv.lunit_braid {Γ : Ctx α ε} {L : LCtx α}
-  : (lunit (φ := φ) (ty := ty) (Γ := Γ) (L := L)) ;; braid = runit := by sorry
+  : (lunit (φ := φ) (ty := ty) (Γ := Γ) (L := L)) ;; braid = runit
+  := by simp only [lunit, ret_pair_braid]; rfl
 
 theorem Eqv.runit_braid {Γ : Ctx α ε} {L : LCtx α}
-  : (runit (φ := φ) (ty := ty) (Γ := Γ) (L := L)) ;; braid = lunit := by sorry
+  : (runit (φ := φ) (ty := ty) (Γ := Γ) (L := L)) ;; braid = lunit
+  := by simp only [runit, ret_pair_braid]; rfl
 
 theorem Eqv.braid_pi_l {Γ : Ctx α ε} {L : LCtx α}
-  : braid ;; pi_l (φ := φ) (A := A) (B := B) (Γ := Γ) (L := L) = pi_r := by sorry
+  : braid ;; pi_l (φ := φ) (A := A) (B := B) (Γ := Γ) (L := L) = pi_r
+  := by simp only [braid, let2_seq, vwk1_pi_l, ret_pair_pi_l]; rfl
 
 theorem Eqv.braid_pi_r {Γ : Ctx α ε} {L : LCtx α}
   : braid ;; pi_r (φ := φ) (A := A) (B := B) (Γ := Γ) (L := L) = pi_l
   := by rw [<-braid_pi_l, <-seq_assoc, braid_braid, nil_seq]
 
 theorem Eqv.rtimes_pi_r {Γ : Ctx α ε} {L : LCtx α}
   (r : Eqv φ (⟨A, ⊥⟩::Γ) (B::L))
-  : Ty.unit ⋊ r ;; pi_r = pi_r ;; r
-  := sorry
+  : Ty.unit ⋊ r ;; pi_r = pi_r ;; r := by
+  simp only [rtimes, let2_seq, vwk1_pi_r, seq_assoc, ret_pair_pi_r]
+  simp only [pi_r, let2_seq]
+  congr 1
+  exact (seq_nil _).trans (nil_seq _).symm
 
 theorem Eqv.ltimes_pi_l {Γ : Ctx α ε} {L : LCtx α}
   (r : Eqv φ (⟨A, ⊥⟩::Γ) (B::L)) : r ⋉ Ty.unit ;; pi_l = pi_l ;; r := by
@@ -271,7 +307,20 @@ theorem Eqv.Pure.central_left {A A' B B' : Ty α} {Γ : Ctx α ε} {L : LCtx α}
   (r : Eqv φ (⟨B, ⊥⟩::Γ) (B'::L))
   : (l ⋉ B) ;; (A' ⋊ r) = (A ⋊ r) ;; (l ⋉ B') := by
   let ⟨p, hp⟩ := hl;
-  simp only [hp, ltimes_eq_ret, ret_seq, Eqv.rtimes]
+  simp only [hp, ltimes_eq_ret, Eqv.rtimes, Eqv.vwk1, ret_seq, vwk_let2, wk_var, Set.mem_setOf_eq,
+    Ctx.InS.coe_wk1, Nat.liftWk_zero, vsubst_let2, var0_subst0, List.length_cons, id_eq,
+    Fin.zero_eta, List.get_eq_getElem, Fin.val_zero, List.getElem_cons_zero, wk_res_self]
+  rw [let2_bind, Term.Eqv.ltimes, Term.Eqv.tensor, let1_let2, let2_seq]
+  apply congrArg
+  simp [
+    let1_beta, Eqv.vwk1, let2_pair, <-ltimes_eq_ret, Eqv.ltimes, Eqv.rtimes, vwk_vwk,
+    ret_seq, vwk_ret, seq_assoc,
+  ]
+  simp [let2_seq, br_zero_eq_ret, ret_pair_braid]
+  simp [
+    Eqv.braid, let2_seq, let2_pair, let1_beta, Eqv.vwk1, vwk_ret, ret_seq, wk_wk,
+    br_zero_eq_ret
+  ]
   sorry
 
 theorem Eqv.Pure.central_right {A A' B B' : Ty α} {Γ : Ctx α ε} {L : LCtx α}

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

@@ -315,28 +315,35 @@ theorem Eqv.Pure.assoc_inv_sum {A B C : Ty α} {Γ : Ctx α ε} {L : LCtx α}
 
 theorem Eqv.assoc_assoc_inv_sum {A B C : Ty α} {Γ : Ctx α ε} {L : LCtx α}
   : assoc_sum (φ := φ) (A := A) (B := B) (C := C) (Γ := Γ) (L := L) ;; assoc_inv_sum = nil
-  := sorry
+  := by rw [<-ret_assoc_sum, <-ret_assoc_inv_sum, <-ret_of_seq, Term.Eqv.assoc_assoc_inv_sum]; rfl
 
 theorem Eqv.assoc_inv_assoc_sum {A B C : Ty α} {Γ : Ctx α ε} {L : LCtx α}
   : assoc_inv_sum (φ := φ) (A := A) (B := B) (C := C) (Γ := Γ) (L := L) ;; assoc_sum = nil
-  := sorry
+  := by rw [<-ret_assoc_sum, <-ret_assoc_inv_sum, <-ret_of_seq, Term.Eqv.assoc_inv_assoc_sum]; rfl
 
 theorem Eqv.assoc_sum_nat {A B C A' B' C' : Ty α} {Γ : Ctx α ε} {L : LCtx α}
   (l : Eqv φ (⟨A, ⊥⟩::Γ) (A'::L)) (m : Eqv φ (⟨B, ⊥⟩::Γ) (B'::L)) (r : Eqv φ (⟨C, ⊥⟩::Γ) (C'::L))
   : sum (sum l m) r ;; assoc_sum = assoc_sum ;; sum l (sum m r)
-  := sorry
+  := by
+  simp only [assoc_sum, sum_seq_coprod, coprod_seq]
+  congr 1
+  · simp only [seq_assoc, inj_l_seq_sum, inj_r_seq_sum]
+    simp only [<-seq_assoc, inj_l_seq_sum]
+  · simp only [seq_assoc, inj_r_seq_sum]; simp only [<-seq_assoc, inj_r_seq_sum]
 
 theorem Eqv.triangle_sum {X Y : Ty α} {Γ : Ctx α ε} {L : LCtx α}
   : assoc_sum (φ := φ) (Γ := Γ) (L := L) (A := X) (B := Ty.empty) (C := Y) ;; nil.sum lzero
-  = rzero.sum nil
-  := sorry
+  = rzero.sum nil := by simp only [
+    assoc_sum, coprod_seq, seq_assoc, lzero, rzero, inj_l_coprod, inj_r_coprod, zero_seq, sum]
 
 theorem Eqv.pentagon_sum {W X Y Z : Ty α} {Γ : Ctx α ε} {L : LCtx α}
   : assoc_sum (φ := φ) (Γ := Γ) (L := L) (A := W.coprod X) (B := Y) (C := Z) ;; assoc_sum
-  = assoc_sum.sum nil ;; assoc_sum ;; nil.sum assoc_sum
-  := sorry
+  = assoc_sum.sum nil ;; assoc_sum ;; nil.sum assoc_sum := by simp only [
+    assoc_sum, sum_seq_coprod, coprod_seq, inj_l_coprod, inj_l_seq_sum, seq_assoc,
+    inj_r_coprod, inj_r_seq_sum, nil_seq
+  ]
 
 theorem Eqv.hexagon_sum {X Y Z : Ty α} {Γ : Ctx α ε} {L : LCtx α}
   : assoc_sum (φ := φ) (Γ := Γ) (L := L) (A := X) (B := Y) (C := Z) ;; braid_sum ;; assoc_sum
-  = braid_sum.sum nil ;; assoc_sum ;; nil.sum braid_sum
-  := sorry
+  = braid_sum.sum nil ;; assoc_sum ;; nil.sum braid_sum := by simp only [
+    braid_sum, assoc_sum, nil_seq, coprod_seq, seq_assoc, inj_r_coprod, inj_l_coprod, sum]

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

@@ -9,6 +9,7 @@ variable [Φ: EffInstSet φ (Ty α) ε] [PartialOrder α] [SemilatticeSup ε] [O
 
 namespace Term
 
+--TODO: seq here is the opposite of seq for region; think about fixing this...
 
 def Eqv.nil {A : Ty α} {Γ : Ctx α ε} : Eqv φ (⟨A, ⊥⟩::Γ) ⟨A, e⟩
   := var 0 (by simp)

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

@@ -291,6 +291,12 @@ def Eqv.coprod {A B C : Ty α} {Γ : Ctx α ε}
   (l : Eqv φ (⟨A, ⊥⟩::Γ) ⟨C, e⟩) (r : Eqv φ (⟨B, ⊥⟩::Γ) ⟨C, e⟩)
   : Eqv φ (⟨A.coprod B, ⊥⟩::Γ) ⟨C, e⟩ := case nil l.wk1 r.wk1
 
+theorem Eqv.coprod_seq {A B C : Ty α} {Γ : Ctx α ε}
+  {l : Eqv φ (⟨A, ⊥⟩::Γ) ⟨C, e⟩} {r : Eqv φ (⟨B, ⊥⟩::Γ) ⟨C, e⟩}
+  {f : Eqv φ (⟨C, ⊥⟩::Γ) ⟨D, e⟩}
+  : coprod l r ;;' f = coprod (l ;;' f) (r ;;' f)
+  := by rw [coprod, seq, let1_case, coprod, wk1_seq, wk1_seq]; rfl
+
 def Eqv.inj_l {A B : Ty α} {Γ : Ctx α ε} : Eqv (φ := φ) (⟨A, ⊥⟩::Γ) ⟨A.coprod B, e⟩
   := inl nil
 
@@ -304,6 +310,11 @@ theorem Eqv.wk2_inj_l {A B : Ty α} {Γ : Ctx α ε}
   : (inj_l (φ := φ) (e := e) (A := A) (B := B) (Γ := head::Γ)).wk2 (inserted := inserted) = inj_l
   := by simp [inj_l]
 
+theorem Eqv.seq_inj_l {A B C : Ty α} {Γ : Ctx α ε} {f : Eqv φ (⟨A, ⊥⟩::Γ) ⟨B, e⟩}
+  : f ;;' inj_l (B := C) = f.inl := by
+  rw [seq, wk1_inj_l, inj_l]
+  exact inl_bind.symm
+
 def Eqv.inj_r {A B : Ty α} {Γ : Ctx α ε} : Eqv (φ := φ) (⟨B, ⊥⟩::Γ) ⟨A.coprod B, e⟩
   := inr nil
 
@@ -317,14 +328,74 @@ theorem Eqv.wk2_inj_r {A B : Ty α} {Γ : Ctx α ε}
   : (inj_r (φ := φ) (e := e) (A := A) (B := B) (Γ := head::Γ)).wk2 (inserted := inserted) = inj_r
   := by simp [inj_r]
 
+theorem Eqv.seq_inj_r {Γ : Ctx α ε} {f : Eqv φ (⟨B, ⊥⟩::Γ) ⟨C, e⟩}
+  : f ;;' inj_r (A := A) = f.inr := by
+  rw [seq, wk1_inj_r, inj_r]
+  exact inr_bind.symm
+
 theorem Eqv.coprod_inl_inr {A B : Ty α} {Γ : Ctx α ε}
   : coprod (Γ := Γ) (e := e) (inj_l (B := B) (φ := φ)) (inj_r (A := A) (φ := φ)) = nil
   := by simp [coprod, inj_l, inj_r, nil, case_eta]
 
+theorem Eqv.inj_l_coprod {B B' C : Ty α} {Γ : Ctx α ε}
+  {g : Eqv φ (⟨B, ⊥⟩::Γ) ⟨C, e⟩}
+  {h : Eqv φ (⟨B', ⊥⟩::Γ) ⟨C, e⟩}
+  : inj_l ;;' coprod g h = g := by
+  rw [inj_l, seq, <-wk_eff_nil (h := bot_le), <-wk_eff_inl, let1_beta, coprod]
+  simp only [wk1_case, wk1_nil, subst_case, nil_subst0, wk_eff_inl, wk_eff_nil]
+  rw [case_inl]
+  convert nil_seq _
+  rw [seq]
+  congr
+  induction g using Quotient.inductionOn
+  apply Eqv.eq_of_term_eq
+  simp only [Set.mem_setOf_eq, InS.coe_subst, Subst.InS.coe_lift, InS.coe_subst0, InS.coe_inl,
+    InS.coe_var, InS.coe_wk, Ctx.InS.coe_wk2, Ctx.InS.coe_wk1, Term.wk_wk]
+  simp only [← Term.subst_fromWk, Term.subst_subst]
+  congr
+  funext k; cases k <;> rfl
+
+theorem Eqv.inl_coprod {A B B' C : Ty α} {Γ : Ctx α ε}
+  {f : Eqv φ (⟨A, ⊥⟩::Γ) ⟨B, e⟩}
+  {g : Eqv φ (⟨B, ⊥⟩::Γ) ⟨C, e⟩}
+  {h : Eqv φ (⟨B', ⊥⟩::Γ) ⟨C, e⟩}
+  : f.inl ;;' coprod g h = f ;;' g := by rw [<-seq_inj_l, <-seq_assoc, inj_l_coprod]
+
+theorem Eqv.inj_r_coprod {B B' C : Ty α} {Γ : Ctx α ε}
+  {g : Eqv φ (⟨B, ⊥⟩::Γ) ⟨C, e⟩}
+  {h : Eqv φ (⟨B', ⊥⟩::Γ) ⟨C, e⟩}
+  : inj_r ;;' coprod g h = h := by
+  rw [inj_r, seq, <-wk_eff_nil (h := bot_le), <-wk_eff_inr, let1_beta, coprod]
+  simp only [wk1_case, wk1_nil, subst_case, nil_subst0, wk_eff_inr, wk_eff_nil]
+  rw [case_inr]
+  convert nil_seq _
+  rw [seq]
+  congr
+  induction h using Quotient.inductionOn
+  apply Eqv.eq_of_term_eq
+  simp only [Set.mem_setOf_eq, InS.coe_subst, Subst.InS.coe_lift, InS.coe_subst0, InS.coe_inl,
+    InS.coe_var, InS.coe_wk, Ctx.InS.coe_wk2, Ctx.InS.coe_wk1, Term.wk_wk]
+  simp only [← Term.subst_fromWk, Term.subst_subst]
+  congr
+  funext k; cases k <;> rfl
+
+theorem Eqv.inr_coprod {A B B' C : Ty α} {Γ : Ctx α ε}
+  {f : Eqv φ (⟨A, ⊥⟩::Γ) ⟨B', e⟩}
+  {g : Eqv φ (⟨B, ⊥⟩::Γ) ⟨C, e⟩}
+  {h : Eqv φ (⟨B', ⊥⟩::Γ) ⟨C, e⟩}
+  : f.inr ;;' coprod g h = f ;;' h := by rw [<-seq_inj_r, <-seq_assoc, inj_r_coprod]
+
 def Eqv.zero {Γ : Ctx α ε} {A : Ty α}
   : Eqv φ (⟨Ty.empty, ⊥⟩::Γ) (A, e)
   := (abort (var 0 (by simp)) A)
 
+theorem Eqv.zero_eq {A : Ty α} {Γ : Ctx α ε}
+  (r s : Eqv φ (⟨Ty.empty, ⊥⟩::Γ) (A, e)) : r = s
+  := by apply Eqv.initial; exact ⟨(Ty.empty, ⊥), by simp, Ty.IsInitial.empty, rfl⟩
+
+theorem Eqv.zero_seq {A B : Ty α} {Γ : Ctx α ε} {f : Eqv φ (⟨A, ⊥⟩::Γ) ⟨B, e⟩}
+  : zero ;;' f = zero := zero_eq _ _
+
 def Eqv.lzero {Γ : Ctx α ε} {A : Ty α}
   : Eqv φ (⟨Ty.empty.coprod A, ⊥⟩::Γ) (A, e)
   := coprod zero nil
@@ -348,19 +419,31 @@ theorem Eqv.braid_braid_sum
   : braid_sum (φ := φ) (A := A) (B := A) (Γ := Γ) (e := e) ;;' braid_sum = nil := by
   rw [braid_sum, seq_swap_sum, seq_nil, swap_sum_swap_sum]
 
+theorem Eqv.braid_sum_def' {A B : Ty α} {Γ : Ctx α ε}
+  : braid_sum (φ := φ) (A := A) (B := B) (Γ := Γ) (e := e) = coprod inj_r inj_l := rfl
+
 def Eqv.assoc_sum {A B C : Ty α} {Γ : Ctx α ε}
   : Eqv φ (⟨(A.coprod B).coprod C, ⊥⟩::Γ) ⟨A.coprod (B.coprod C), e⟩
   := nil.reassoc_sum
 
--- theorem Eqv.assoc_sum_def' {A B C : Ty α} {Γ : Ctx α ε}
---   : assoc_sum (φ := φ) (A := A) (B := B) (C := C) (Γ := Γ) (e := e)
---   = coprod (coprod inj_l (inj_l ;;' inj_r)) (inj_r ;;' inj_r)
---   := by simp [coprod, assoc_sum, reassoc_sum, wk1_seq, wk2_seq]; sorry
+theorem Eqv.assoc_sum_def' {A B C : Ty α} {Γ : Ctx α ε}
+  : assoc_sum (φ := φ) (A := A) (B := B) (C := C) (Γ := Γ) (e := e)
+  = coprod (coprod inj_l (inj_l ;;' inj_r)) (inj_r ;;' inj_r) := by
+  simp only [assoc_sum, reassoc_sum, coprod, wk1_inj_l, wk1_seq, wk1_inj_r, wk1_case, wk1_nil,
+    wk2_inj_l, wk2_seq, wk2_inj_r, seq_inj_r, seq_inj_l]
+  rfl
 
 def Eqv.assoc_inv_sum {A B C : Ty α} {Γ : Ctx α ε}
   : Eqv φ (⟨A.coprod (B.coprod C), ⊥⟩::Γ) ⟨(A.coprod B).coprod C, e⟩
   := nil.reassoc_inv_sum
 
+theorem Eqv.assoc_inv_sum_def' {A B C : Ty α} {Γ : Ctx α ε}
+  : assoc_inv_sum (φ := φ) (A := A) (B := B) (C := C) (Γ := Γ) (e := e)
+  = coprod (inj_l ;;' inj_l) (coprod (inj_r ;;' inj_l) inj_r) := by
+  simp only [assoc_inv_sum, reassoc_inv_sum, coprod, wk1_inj_l, wk1_seq, wk1_inj_r, wk1_case,
+    wk1_nil, wk2_inj_l, wk2_seq, wk2_inj_r, seq_inj_r, seq_inj_l]
+  rfl
+
 theorem Eqv.assoc_assoc_inv_sum
   : assoc_sum (φ := φ) (A := A) (B := B) (C := C) (Γ := Γ) (e := e) ;;' assoc_inv_sum = nil := by
   rw [assoc_sum, assoc_inv_sum, seq_reassoc_inv_sum, seq_nil, reassoc_inv_reassoc_sum]
@@ -369,6 +452,32 @@ theorem Eqv.assoc_inv_assoc_sum
   : assoc_inv_sum (φ := φ) (A := A) (B := B) (C := C) (Γ := Γ) (e := e) ;;' assoc_sum = nil := by
   rw [assoc_sum, assoc_inv_sum, seq_reassoc_sum, seq_nil, reassoc_reassoc_inv_sum]
 
+theorem Eqv.assoc_sum_nat {A B C A' B' C' : Ty α} {Γ : Ctx α ε}
+  (l : Eqv φ (⟨A, ⊥⟩::Γ) (A', e)) (m : Eqv φ (⟨B, ⊥⟩::Γ) (B', e)) (r : Eqv φ (⟨C, ⊥⟩::Γ) (C', e))
+  : sum (sum l m) r ;;' assoc_sum = assoc_sum ;;' sum l (sum m r)
+  := by simp only [
+    sum, coprod_seq, <-seq_assoc, inj_l_coprod, inj_r_coprod, assoc_sum_def'
+  ]
+
+theorem Eqv.triangle_sum {X Y : Ty α} {Γ : Ctx α ε}
+  : assoc_sum (φ := φ) (Γ := Γ) (e := e) (A := X) (B := Ty.empty) (C := Y) ;;' nil.sum lzero
+  = rzero.sum nil := by simp only [
+    assoc_sum_def', coprod_seq, <-seq_assoc, lzero, rzero, inj_l_coprod, inj_r_coprod, zero_seq, sum
+  ]
+
+theorem Eqv.pentagon_sum {W X Y Z : Ty α} {Γ : Ctx α ε}
+  : assoc_sum (φ := φ) (Γ := Γ) (e := e) (A := W.coprod X) (B := Y) (C := Z) ;;' assoc_sum
+  = assoc_sum.sum nil ;;' assoc_sum ;;' nil.sum assoc_sum := by simp only [
+    assoc_sum_def', coprod_seq, inj_l_coprod, <-seq_assoc, inj_r_coprod, nil_seq, sum
+  ]
+
+theorem Eqv.hexagon_sum {X Y Z : Ty α} {Γ : Ctx α ε}
+  : assoc_sum (φ := φ) (Γ := Γ) (e := e) (A := X) (B := Y) (C := Z) ;;' braid_sum ;;' assoc_sum
+  = braid_sum.sum nil ;;' assoc_sum ;;' nil.sum braid_sum := by simp only [
+    braid_sum_def', assoc_sum_def', nil_seq, coprod_seq, <-seq_assoc, inj_r_coprod, inj_l_coprod,
+    sum
+  ]
+
 -- TODO: assoc is natural
 
 -- TODO: lzero, rzero are natural

DeBruijnSSA/BinSyntax/Rewrite/Term/Eqv.lean

@@ -1680,6 +1680,27 @@ theorem Eqv.Pure.let2_let1_of_left {Γ : Ctx α ε}
   : let2 b (let1 a' c') = let1 a (let2 b.wk0 c) := by
     rw [ha.let1_let2_of_right, ha', hc']
 
+theorem Eqv.inl_bind {Γ : Ctx α ε} {a : Eqv φ Γ ⟨A, e⟩}
+  : a.inl (B := B) = let1 a (inl (var 0 (by simp))) := calc
+  _ = let1 a.inl (var 0 Ctx.Var.bhead) := by rw [let1_eta]
+  _ = let1 a (let1 (inl (var 0 Ctx.Var.bhead)) (var 0 Ctx.Var.bhead)) := by rw [let1_inl, wk1_var0]
+  _ = let1 a (let1 (wk_eff bot_le (inl (var 0 Ctx.Var.shead))) (var 0 Ctx.Var.bhead)) := by rfl
+  _ = _ := by rw [let1_beta]; rfl
+
+theorem Eqv.inr_bind {Γ : Ctx α ε} {a : Eqv φ Γ ⟨A, e⟩}
+  : a.inr (A := B) = let1 a (inr (var 0 (by simp))) := calc
+  _ = let1 a.inr (var 0 Ctx.Var.bhead) := by rw [let1_eta]
+  _ = let1 a (let1 (inr (var 0 Ctx.Var.bhead)) (var 0 Ctx.Var.bhead)) := by rw [let1_inr, wk1_var0]
+  _ = let1 a (let1 (wk_eff bot_le (inr (var 0 Ctx.Var.shead))) (var 0 Ctx.Var.bhead)) := by rfl
+  _ = _ := by rw [let1_beta]; rfl
+
+-- theorem Eqv.inl_let1 {Γ : Ctx α ε} {a : Eqv φ Γ ⟨A, e⟩} {b : Eqv φ ((A, ⊥)::Γ) ⟨B, e⟩}
+--   : (let1 a b).inl = let1 a (b.inl (B := C)) := calc
+--   _ = (let1 (let1 a b) (var 0 (by simp))).inl := by rw [let1_eta]
+--   _ = (let1 a (let1 b (var 0 (by simp)))).inl := by rw [let1_let1, wk1_var0]
+--   _ = (let1 a (let1 b (var 0 (by simp))).inl) := by sorry
+--   _ = _ := sorry
+
 end Basic
 
 end Term