diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Completeness.lean b/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Completeness.lean
index 7d30cf3..21f2312 100644
--- a/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Completeness.lean
+++ b/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Completeness.lean
@@ -196,12 +196,17 @@ theorem Eqv.packed_cfg_den {Γ : Ctx α ε} {L R : LCtx α} {β : Eqv φ Γ (R +
   = (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
-          )
+        ret split ⋉ R.pack ;; assoc ;; Γ.pack ⋊ (ret distl_pack
+          ;; pack_coprod (λ i =>
+            acast R.get_dist ;; (G (Fin.cast R.length_dist i)).packed)
+          ;; ret Term.Eqv.pack_app
+        ) ;; distl_inv ;; sum pi_r nil
+        -- 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
@@ -256,5 +261,7 @@ 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]
+    apply congrArg
+    apply congrArg
     sorry
diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Region/Structural/Sum.lean b/DeBruijnSSA/BinSyntax/Rewrite/Region/Structural/Sum.lean
index 643b65d..c7ebd01 100644
--- a/DeBruijnSSA/BinSyntax/Rewrite/Region/Structural/Sum.lean
+++ b/DeBruijnSSA/BinSyntax/Rewrite/Region/Structural/Sum.lean
@@ -655,6 +655,11 @@ theorem Eqv.packed_out_binary_ret_seq  {Γ : Ctx α ε}
       Term.Eqv.inj_n, sum, coprod, case_inl, Term.Eqv.nil, let1_beta, inj_l
     ]
 
+theorem Eqv.packed_out_ret_seq {Γ : Ctx α ε}
+  {c : Term.Eqv φ ((X, ⊥)::Γ) (Y, ⊥)} {r : Eqv φ ((Y, ⊥)::Γ) (A::L)}
+  : (ret c ;; r).packed_out = ret c ;; r.packed_out := by
+  simp [ret_seq, vsubst_packed_out, vwk1_packed_out]
+
 theorem Eqv.packed_out_unpacked_app_out_inner  {Γ : Ctx α ε} {R L : LCtx α}
   {r : Eqv φ ((X, ⊥)::Γ) [(R ++ L).pack]}
   : r.unpacked_app_out.packed_out