Reduced completeness to lore

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

@@ -266,8 +266,23 @@ theorem Eqv.packed_cfg_den {Γ : Ctx α ε} {L R : LCtx α} {β : Eqv φ Γ (R +
     rfl
   · rw [fixpoint_def']
     congr 5
-    simp [seq_assoc, ltimes_eq_ret, assoc_eq_ret, packed_out_ret_seq]
+    simp only [LCtx.pack.eq_2, LCtx.pack.eq_1, ltimes_eq_ret, assoc_eq_ret, List.get_eq_getElem,
+      Fin.coe_cast, seq_assoc, packed_out_ret_seq]
     apply congrArg
     apply congrArg
-    --simp only [unpacked_app_out_eq_left_exit]
-    sorry
+    conv =>
+      lhs
+      rw [
+        packed_out_binary_rtimes, packed_out_unpacked_app_out, <-rtimes_rtimes,
+        seq_assoc (right := distl_inv), rtimes_sum_seq_distl_inv,
+        seq_assoc (right := sum _ _), seq_assoc (right := coprod _ _)
+      ]
+    congr 1
+    · rw [seq_assoc]
+    · rw [seq_assoc, seq_assoc]
+      apply congrArg
+      rw [
+        sum_seq_coprod, sum_seq_coprod, nil_seq, rtimes_nil, nil_seq, <-seq_assoc,
+        rtimes_pi_r, seq_assoc, inj_r_coprod
+      ]
+      rfl

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

@@ -88,3 +88,8 @@ 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.rtimes_sum_seq_distl_inv {A B C : Ty α} {Γ : Ctx α ε} {L : LCtx α}
+  {l : Eqv φ ((A, ⊥)::Γ) (A'::L)} {r : Eqv φ ((B, ⊥)::Γ) (B'::L)}
+  : C ⋊ (sum l r) ;; distl_inv = distl_inv ;; sum (C ⋊ l) (C ⋊ r)
+  := sorry

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

@@ -360,14 +360,14 @@ theorem Eqv.braid_pi_r {Γ : Ctx α ε} {L : LCtx α}
 
 theorem Eqv.rtimes_pi_r {Γ : Ctx α ε} {L : LCtx α}
   (r : Eqv φ (⟨A, ⊥⟩::Γ) (B::L))
-  : Ty.unit ⋊ r ;; pi_r = pi_r ;; r := by
+  : C ⋊ 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
+  (r : Eqv φ (⟨A, ⊥⟩::Γ) (B::L)) : r ⋉ C ;; pi_l = pi_l ;; r := by
   rw [<-braid_rtimes_braid, seq_assoc, braid_pi_l, seq_assoc, rtimes_pi_r, <-seq_assoc, braid_pi_r]
 
 theorem Eqv.let2_tensor_vwk2 {Γ : Ctx α ε} {L : LCtx α}