diff --git a/DataflowRewriter/Examples/BranchMerge.lean b/DataflowRewriter/Examples/BranchMerge.lean
index 31f321c..27cb8a3 100644
--- a/DataflowRewriter/Examples/BranchMerge.lean
+++ b/DataflowRewriter/Examples/BranchMerge.lean
@@ -13,7 +13,6 @@ namespace DataflowRewriter
 
 section BranchMerge
 
-
   -- TODO how to do polymorphic definition, here [out] is hardcoded and should be parametrized?
   -- TODO refer to other graph with proper namespacing, semantics either inline or do environment business
   -- TODO potentially woudl it be possible to automatically construct the environment if I use nonstrings.
diff --git a/DataflowRewriter/ExprLow.lean b/DataflowRewriter/ExprLow.lean
index 4d04c49..336f7c5 100644
--- a/DataflowRewriter/ExprLow.lean
+++ b/DataflowRewriter/ExprLow.lean
@@ -432,23 +432,16 @@ theorem substition {I I' i i' mod mod' iexpr} :
       rw [this]; simp [drunfold,Module.refines_reflexive]
   | product e₁ e₂ ihe₁ ihe₂ =>
     intro hwf hf₁ hf₂ href
-    apply refines_product
-    · simp [all, wf] at hwf ⊢; simp [hwf]
-    · simp [all, wf] at hwf ⊢; simp [hwf]
-    · have : e₁.wf ε := by simp_all [all,wf]
-      apply wf_modify_expression
-      simp only [*]; simp
-      assumption
-    · have : e₂.wf ε := by simp_all [all,wf]
-      apply wf_modify_expression
-      simp only [*]; simp
-      assumption
-    · have : e₁.wf ε := by simp_all [all,wf]
-      solve_by_elim
-    · have : e₂.wf ε := by simp_all [all,wf]
-      solve_by_elim
-  | _ => sorry
-
+    have e₁wf : e₁.wf ε := by simp [all, wf] at hwf ⊢; simp [hwf]
+    have e₂wf : e₂.wf ε := by simp [all, wf] at hwf ⊢; simp [hwf]
+    have some_isSome : (ε.find? i').isSome := by simp only [*]; simp
+    apply refines_product <;> solve_by_elim [wf_modify_expression]
+  | connect o i e =>
+    intro hwf hfind₁ hfind₂ href
+    simp only [modify]
+    have e₁wf : e.wf ε := by simp [all, wf] at hwf ⊢; simp [hwf]
+    have some_isSome : (ε.find? i').isSome := by simp only [*]; simp
+    apply refines_connect <;> solve_by_elim [wf_modify_expression]
 
 set_option debug.byAsSorry true
 theorem abstract_refines {iexpr expr_pat i} :