diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Region/Eqv.lean b/DeBruijnSSA/BinSyntax/Rewrite/Region/Eqv.lean
index ae43d78..2b5faa8 100644
--- a/DeBruijnSSA/BinSyntax/Rewrite/Region/Eqv.lean
+++ b/DeBruijnSSA/BinSyntax/Rewrite/Region/Eqv.lean
@@ -1,5 +1,6 @@
 import DeBruijnSSA.BinSyntax.Rewrite.Region.Setoid
 import DeBruijnSSA.BinSyntax.Rewrite.Term.Eqv
+import DeBruijnSSA.BinSyntax.Rewrite.Term.Case
 
 import Discretion.Utils.Quotient
 
@@ -980,24 +981,6 @@ theorem Eqv.let1_let2 {Γ : Ctx α ε} {L : LCtx α} {A B : Ty α}
   induction b using Quotient.inductionOn
   apply Eqv.sound; apply InS.let1_let2
 
-theorem Eqv.let1_inl {Γ : Ctx α ε} {L : LCtx α} {A B : Ty α} (e' := ⊥)
-  {r : Eqv φ (⟨A.coprod B, ⊥⟩::Γ) L}
-  (a : Term.Eqv φ Γ ⟨A, e⟩)
-    : Eqv.let1 a.inl r
-    = (r.vwk1.let1 ((var 0 (by simp)).inl (e := e'))).let1 a := by
-  induction a using Quotient.inductionOn
-  induction r using Quotient.inductionOn
-  apply Eqv.sound; apply InS.let1_inl
-
-theorem Eqv.let1_inr {Γ : Ctx α ε} {L : LCtx α} {A B : Ty α} (e' := ⊥)
-  {r : Eqv φ (⟨A.coprod B, ⊥⟩::Γ) L}
-  (b : Term.Eqv φ Γ ⟨B, e⟩)
-    : Eqv.let1 b.inr r
-    = (r.vwk1.let1 ((var 0 (by simp)).inr (e := e'))).let1 b := by
-  induction b using Quotient.inductionOn
-  induction r using Quotient.inductionOn
-  apply Eqv.sound; apply InS.let1_inr
-
 theorem Eqv.let1_case {Γ : Ctx α ε} {L : LCtx α} {A B : Ty α}
   {s : Eqv φ (⟨C, ⊥⟩::Γ) L}
   (a : Term.Eqv φ Γ ⟨Ty.coprod A B, e⟩)
@@ -1010,15 +993,6 @@ theorem Eqv.let1_case {Γ : Ctx α ε} {L : LCtx α} {A B : Ty α}
   induction s using Quotient.inductionOn
   apply Eqv.sound; apply InS.let1_case
 
-theorem Eqv.let1_abort {Γ : Ctx α ε} {L : LCtx α} {A : Ty α} (e' := ⊥)
-  {r : Eqv φ (⟨A, ⊥⟩::Γ) L}
-  (a : Term.Eqv φ Γ ⟨Ty.empty, e⟩)
-    : Eqv.let1 (a.abort _) r
-    = (r.vwk1.let1 ((var 0 (by simp)).abort (e := e') _)).let1 a := by
-  induction a using Quotient.inductionOn
-  induction r using Quotient.inductionOn
-  apply Eqv.sound; apply InS.let1_abort
-
 theorem Eqv.let2_bind {Γ : Ctx α ε} {L : LCtx α}
   {e : Term.Eqv φ Γ ⟨A.prod B, e⟩} {r : Eqv φ (⟨B, ⊥⟩::⟨A, ⊥⟩::Γ) L}
   : let2 e r
@@ -1233,6 +1207,31 @@ theorem Eqv.case_inr {Γ : Ctx α ε} {L : LCtx α}
   induction s using Quotient.inductionOn
   case _ e r s => exact Eqv.sound (InS.case_inr e r s)
 
+theorem Eqv.let1_inl {Γ : Ctx α ε} {L : LCtx α} {A B : Ty α} (e' := ⊥)
+  {r : Eqv φ (⟨A.coprod B, ⊥⟩::Γ) L}
+  (a : Term.Eqv φ Γ ⟨A, e⟩)
+    : Eqv.let1 a.inl r
+    = (r.vwk1.let1 ((var 0 (by simp)).inl (e := e'))).let1 a := by
+  rw [<-Term.Eqv.case_eta (a := inl a), let1_case, case_inl]
+  rfl
+
+theorem Eqv.let1_inr {Γ : Ctx α ε} {L : LCtx α} {A B : Ty α} (e' := ⊥)
+  {r : Eqv φ (⟨A.coprod B, ⊥⟩::Γ) L}
+  (b : Term.Eqv φ Γ ⟨B, e⟩)
+    : Eqv.let1 b.inr r
+    = (r.vwk1.let1 ((var 0 (by simp)).inr (e := e'))).let1 b := by
+  rw [<-Term.Eqv.case_eta (a := inr b), let1_case, case_inr]
+  rfl
+
+theorem Eqv.let1_abort {Γ : Ctx α ε} {L : LCtx α} {A : Ty α} (e' := ⊥)
+  {r : Eqv φ (⟨A, ⊥⟩::Γ) L}
+  (a : Term.Eqv φ Γ ⟨Ty.empty, e⟩)
+    : Eqv.let1 (a.abort _) r
+    = (r.vwk1.let1 ((var 0 (by simp)).abort (e := e') _)).let1 a := by
+  induction a using Quotient.inductionOn
+  induction r using Quotient.inductionOn
+  apply Eqv.sound; apply InS.let1_abort
+
 -- TODO: Eqv.dead_cfg_left
 
 theorem Eqv.let1_beta {Γ : Ctx α ε} {L : LCtx α}
diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Region/Setoid.lean b/DeBruijnSSA/BinSyntax/Rewrite/Region/Setoid.lean
index b79f6d8..4e9d97a 100644
--- a/DeBruijnSSA/BinSyntax/Rewrite/Region/Setoid.lean
+++ b/DeBruijnSSA/BinSyntax/Rewrite/Region/Setoid.lean
@@ -212,20 +212,6 @@ theorem InS.let1_let2 {Γ : Ctx α ε} {L : LCtx α} {A B : Ty α}
     ≈ (let2 a $ let1 b $ r.vwk1.vwk1)
   := Uniform.rel $ TStep.rewrite InS.coe_wf InS.coe_wf (by constructor)
 
-theorem InS.let1_inl {Γ : Ctx α ε} {L : LCtx α} {A B : Ty α} (e' := ⊥)
-  {r : InS φ (⟨A.coprod B, ⊥⟩::Γ) L}
-  (a : Term.InS φ Γ ⟨A, e⟩)
-    : r.let1 a.inl
-    ≈ (r.vwk1.let1 ((var 0 (by simp)).inl (e := e'))).let1 a
-  := Uniform.rel $ TStep.rewrite InS.coe_wf InS.coe_wf (by constructor)
-
-theorem InS.let1_inr {Γ : Ctx α ε} {L : LCtx α} {A B : Ty α} (e' := ⊥)
-  {r : InS φ (⟨A.coprod B, ⊥⟩::Γ) L}
-  (b : Term.InS φ Γ ⟨B, e⟩)
-    : r.let1 b.inr
-    ≈ (r.vwk1.let1 ((var 0 (by simp)).inr (e := e'))).let1 b
-  := Uniform.rel $ TStep.rewrite InS.coe_wf InS.coe_wf (by constructor)
-
 theorem InS.let1_case {Γ : Ctx α ε} {L : LCtx α} {A B : Ty α}
   {s : InS φ (⟨C, ⊥⟩::Γ) L}
   (a : Term.InS φ Γ ⟨Ty.coprod A B, e⟩)
diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Region/Step.lean b/DeBruijnSSA/BinSyntax/Rewrite/Region/Step.lean
index 452c316..066bb93 100644
--- a/DeBruijnSSA/BinSyntax/Rewrite/Region/Step.lean
+++ b/DeBruijnSSA/BinSyntax/Rewrite/Region/Step.lean
@@ -1,5 +1,6 @@
 import DeBruijnSSA.BinSyntax.Typing.Region
-import DeBruijnSSA.BinSyntax.Syntax.Rewrite.Region.Step
+import DeBruijnSSA.BinSyntax.Syntax.Rewrite.Region.Rewrite
+import DeBruijnSSA.BinSyntax.Syntax.Rewrite.Region.Reduce
 import DeBruijnSSA.BinSyntax.Rewrite.Region.Cong
 import DeBruijnSSA.BinSyntax.Rewrite.Term.Setoid
 
diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Region/Typing.lean b/DeBruijnSSA/BinSyntax/Rewrite/Region/Typing.lean
deleted file mode 100644
index 077b177..0000000
--- a/DeBruijnSSA/BinSyntax/Rewrite/Region/Typing.lean
+++ /dev/null
@@ -1,91 +0,0 @@
-import DeBruijnSSA.BinSyntax.Typing.Region
-import DeBruijnSSA.BinSyntax.Syntax.Rewrite
-
-import Discretion.Utils.Quotient
-
-namespace BinSyntax
-
-variable [Φ: EffInstSet φ (Ty α) ε] [PartialOrder α] [SemilatticeSup ε] [OrderBot ε]
-
--- TODO: rewrite to use subst.cons...
-
--- def Term.WfD.subst₂ {Γ : Ctx α ε} {a b : Term φ}
---   (ha : a.WfD Γ ⟨A, e⟩) (hb : b.WfD Γ ⟨B, e'⟩)
---   : (a.subst₂ b).WfD Γ (⟨A, e⟩::⟨B, e'⟩::Γ)
---   | ⟨0, _⟩ => ha
---   | ⟨1, _⟩ => hb
---   | ⟨n + 2, h⟩ => var ⟨by simp at h; exact h, le_refl _⟩
-
--- namespace Region
-
--- structure HaveTrg (Γ : Ctx α ε) (L : LCtx α) (r r' : Region φ) where
---   left : r.WfD Γ L
---   right : r'.WfD Γ L
-
--- -- TODO: therefore, a prefunctor to HaveTrg lifts via CongD...
-
--- def RewriteD.wfD {Γ : Ctx α ε} {r r' : Region φ} {L}
---   : RewriteD r r' → r.WfD Γ L → r'.WfD Γ L
---   | let1_op f e r, WfD.let1 (Term.WfD.op hf he) hr
---     => WfD.let1 he (WfD.let1 (Term.WfD.op hf Term.WfD.var0_pure) hr.vwk1)
---   | let1_pair a b r, WfD.let1 (Term.WfD.pair ha hb) hr
---     => WfD.let1 ha $
---       WfD.let1 hb.wk0 $
---       WfD.let1 (Term.WfD.pair Term.WfD.var1 Term.WfD.var0) hr.vwk1.vwk1
---   | let1_inl a r, WfD.let1 (Term.WfD.inl ha) hr
---     => WfD.let1 ha $ WfD.let1 (Term.WfD.inl Term.WfD.var0) hr.vwk1
---   | let1_inr b r, WfD.let1 (Term.WfD.inr hb) hr
---     => WfD.let1 hb $ WfD.let1 (Term.WfD.inr Term.WfD.var0) hr.vwk1
---   | let1_abort A r, WfD.let1 (Term.WfD.abort ha) hr
---     => WfD.let1 ha $ WfD.let1 (Term.WfD.abort Term.WfD.var0) hr.vwk1
---   | let2_op f e r, WfD.let2 (Term.WfD.op hf he) hr
---     => WfD.let1 he
---       (WfD.let2 (Term.WfD.op hf Term.WfD.var0_pure)
---       (hr.vwk (by simp [Nat.liftnWk_two])))
---   | let2_pair a b r, _ => sorry
---   | let2_abort e r, _ => sorry
---   | case_op f e r s, _ => sorry
---   | case_abort e r s, _ => sorry
---   | let1_case a b r s, _ => sorry
---   | let2_case a b r s, _ => sorry
---   | cfg_br_lt ℓ e n G h, _ => sorry
---   | cfg_let1 a β n G, _ => sorry
---   | cfg_let2 a β n G, _ => sorry
---   | cfg_case e r s n G, _ => sorry
---   | cfg_cfg β n G n' G', _ => sorry
---   | cfg_zero β G, WfD.cfg _ [] rfl dβ dG => dβ
---   | cfg_fuse β n G k ρ hρ, WfD.cfg _ R hR dβ dG => sorry
---   | let2_eta e r, _ => sorry
-
--- def RewriteD.wfD_inv {Γ : Ctx α ε} {r r' : Region φ} {L}
---   : RewriteD r r' → r'.WfD Γ L → r.WfD Γ L
---   | let1_op f e r, WfD.let1 (A := A) he (WfD.let1 (Term.WfD.op hf hv) hr)
---     => sorry --WfD.let1 (Term.WfD.op sorry he) sorry
---   | let1_pair a b r, _ => sorry
---   | let1_inl a r, _ => sorry
---   | let1_inr b r, _ => sorry
---   | let1_abort A r, _ => sorry
---   | let2_op f e r, _=> sorry
---   | let2_pair a b r, _ => sorry
---   | let2_abort e r, _ => sorry
---   | case_op f e r s, _ => sorry
---   | case_abort e r s, _ => sorry
---   | let1_case a b r s, _ => sorry
---   | let2_case a b r s, _ => sorry
---   | cfg_br_lt ℓ e n G h, _ => sorry
---   | cfg_let1 a β n G, _ => sorry
---   | cfg_let2 a β n G, _ => sorry
---   | cfg_case e r s n G, _ => sorry
---   | cfg_cfg β n G n' G', _ => sorry
---   | cfg_zero β G, dβ => WfD.cfg 0 [] rfl dβ (λi => i.elim0)
---   | cfg_fuse β n G k ρ hρ, WfD.cfg _ R hR dβ dG => sorry
---   | let2_eta e r, _ => sorry
-
--- def ReduceD.wfD {Γ : Ctx α ε} {r r' : Region φ} {L}
---   : ReduceD r r' → r.WfD Γ L → r'.WfD Γ L
---   | case_inl e r s, WfD.case (Term.WfD.inl de) dr ds => dr.let1 de
---   | case_inr e r s, WfD.case (Term.WfD.inr de) dr ds => ds.let1 de
---   | wk_cfg β n G k ρ, WfD.cfg _ R hR dβ dG =>
---     sorry
---   | dead_cfg_left β n G m G', WfD.cfg _ R hR dβ dG =>
---     sorry
diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Term/Case.lean b/DeBruijnSSA/BinSyntax/Rewrite/Term/Case.lean
index 7e103fc..e583f76 100644
--- a/DeBruijnSSA/BinSyntax/Rewrite/Term/Case.lean
+++ b/DeBruijnSSA/BinSyntax/Rewrite/Term/Case.lean
@@ -215,6 +215,46 @@ theorem Eqv.case_let1_wk0_pure {Γ : Ctx α ε}
 
 -- TODO: derive these...
 
+theorem Eqv.let1_inl {Γ : Ctx α ε} {a : Eqv φ Γ ⟨A, e⟩} {r : Eqv φ (⟨Ty.coprod A B, ⊥⟩::Γ) ⟨C, e⟩}
+  : let1 (inl a) r = (let1 a $ let1 (inl (var 0 (by simp))) $ r.wk1) := by
+  rw [<-case_eta (a := inl a), let1_case, case_inl]
+
+theorem Eqv.let1_inr {Γ : Ctx α ε} {a : Eqv φ Γ ⟨B, e⟩} {r : Eqv φ (⟨Ty.coprod A B, ⊥⟩::Γ) ⟨C, e⟩}
+  : let1 (inr a) r = (let1 a $ let1 (inr (var 0 (by simp))) $ r.wk1) := by
+  rw [<-case_eta (a := inr a), let1_case, case_inr]
+
+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)) := by
+  rw [inl_bind, let1_let1, wk1_inl, wk1_var0, <-inl_bind]
+
+theorem Eqv.inr_let1 {Γ : Ctx α ε} {a : Eqv φ Γ ⟨A, e⟩} {b : Eqv φ ((A, ⊥)::Γ) ⟨B, e⟩}
+  : (let1 a b).inr = let1 a (b.inr (A := C)) := by
+  rw [inr_bind, let1_let1, wk1_inr, wk1_var0, <-inr_bind]
+
+theorem Eqv.inl_let2 {Γ : Ctx α ε}
+  {a : Eqv φ Γ ⟨A.prod B, e⟩} {b : Eqv φ ((B, ⊥)::(A, ⊥)::Γ) ⟨C, e⟩}
+  : (let2 a b).inl = let2 a (b.inl (B := D)) := by
+  rw [inl_bind, let1_let2, wk1_inl, wk1_inl, wk1_var0, wk1_var0, <-inl_bind]
+
+theorem Eqv.inr_let2 {Γ : Ctx α ε}
+  {a : Eqv φ Γ ⟨A.prod B, e⟩} {b : Eqv φ ((B, ⊥)::(A, ⊥)::Γ) ⟨C, e⟩}
+  : (let2 a b).inr = let2 a (b.inr (A := D)) := by
+  rw [inr_bind, let1_let2, wk1_inr, wk1_inr, wk1_var0, wk1_var0, <-inr_bind]
+
 theorem Eqv.case_inl_inl {Γ : Ctx α ε}
   {a : Eqv φ Γ ⟨A.coprod B, e⟩}
   {r : Eqv φ (⟨A, ⊥⟩::Γ) ⟨C, e⟩}
diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Term/Eqv.lean b/DeBruijnSSA/BinSyntax/Rewrite/Term/Eqv.lean
index 2695578..3812a87 100644
--- a/DeBruijnSSA/BinSyntax/Rewrite/Term/Eqv.lean
+++ b/DeBruijnSSA/BinSyntax/Rewrite/Term/Eqv.lean
@@ -1029,18 +1029,6 @@ theorem Eqv.let1_let2_inv {Γ : Ctx α ε} {a : Eqv φ Γ ⟨Ty.prod A B, e⟩}
   (h : r' = r.wk1.wk1)
   :  (let2 a $ let1 b $ r') = let1 (let2 a b) r := by cases h; rw [let1_let2]
 
-theorem Eqv.let1_inl {Γ : Ctx α ε} {a : Eqv φ Γ ⟨A, e⟩} {r : Eqv φ (⟨Ty.coprod A B, ⊥⟩::Γ) ⟨C, e⟩}
-  : let1 (inl a) r = (let1 a $ let1 (inl (var 0 (by simp))) $ r.wk1) := by
-  induction a using Quotient.inductionOn
-  induction r using Quotient.inductionOn
-  apply Eqv.sound; apply InS.let1_inl
-
-theorem Eqv.let1_inr {Γ : Ctx α ε} {a : Eqv φ Γ ⟨B, e⟩} {r : Eqv φ (⟨Ty.coprod A B, ⊥⟩::Γ) ⟨C, e⟩}
-  : let1 (inr a) r = (let1 a $ let1 (inr (var 0 (by simp))) $ r.wk1) := by
-  induction a using Quotient.inductionOn
-  induction r using Quotient.inductionOn
-  apply Eqv.sound; apply InS.let1_inr
-
 theorem Eqv.let1_case {Γ : Ctx α ε} {a : Eqv φ Γ ⟨Ty.coprod A B, e⟩}
   {l : Eqv φ (⟨A, ⊥⟩::Γ) ⟨C, e⟩} {r : Eqv φ (⟨B, ⊥⟩::Γ) ⟨C, e⟩}
   {s : Eqv φ (⟨C, ⊥⟩::Γ) ⟨D, e⟩}
@@ -1600,38 +1588,6 @@ 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)) := by
-  rw [inl_bind, let1_let1, wk1_inl, wk1_var0, <-inl_bind]
-
-theorem Eqv.inr_let1 {Γ : Ctx α ε} {a : Eqv φ Γ ⟨A, e⟩} {b : Eqv φ ((A, ⊥)::Γ) ⟨B, e⟩}
-  : (let1 a b).inr = let1 a (b.inr (A := C)) := by
-  rw [inr_bind, let1_let1, wk1_inr, wk1_var0, <-inr_bind]
-
-theorem Eqv.inl_let2 {Γ : Ctx α ε}
-  {a : Eqv φ Γ ⟨A.prod B, e⟩} {b : Eqv φ ((B, ⊥)::(A, ⊥)::Γ) ⟨C, e⟩}
-  : (let2 a b).inl = let2 a (b.inl (B := D)) := by
-  rw [inl_bind, let1_let2, wk1_inl, wk1_inl, wk1_var0, wk1_var0, <-inl_bind]
-
-theorem Eqv.inr_let2 {Γ : Ctx α ε}
-  {a : Eqv φ Γ ⟨A.prod B, e⟩} {b : Eqv φ ((B, ⊥)::(A, ⊥)::Γ) ⟨C, e⟩}
-  : (let2 a b).inr = let2 a (b.inr (A := D)) := by
-  rw [inr_bind, let1_let2, wk1_inr, wk1_inr, wk1_var0, wk1_var0, <-inr_bind]
-
 end Basic
 
 end Term
diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Term/Setoid.lean b/DeBruijnSSA/BinSyntax/Rewrite/Term/Setoid.lean
index a283614..6fd5c90 100644
--- a/DeBruijnSSA/BinSyntax/Rewrite/Term/Setoid.lean
+++ b/DeBruijnSSA/BinSyntax/Rewrite/Term/Setoid.lean
@@ -137,14 +137,6 @@ theorem InS.let1_let2 {Γ : Ctx α ε} {a : InS φ Γ ⟨Ty.prod A B, e⟩}
   : let1 (let2 a b) r ≈ (let2 a $ let1 b $ r.wk1.wk1)
   := Uniform.rel $ TStep.rewrite InS.coe_wf InS.coe_wf (by constructor)
 
-theorem InS.let1_inl {Γ : Ctx α ε} {a : InS φ Γ ⟨A, e⟩} {r : InS φ (⟨Ty.coprod A B, ⊥⟩::Γ) ⟨C, e⟩}
-  : let1 (inl a) r ≈ (let1 a $ let1 (inl (var 0 (by simp))) $ r.wk1)
-  := Uniform.rel $ TStep.rewrite InS.coe_wf InS.coe_wf (by constructor)
-
-theorem InS.let1_inr {Γ : Ctx α ε} {a : InS φ Γ ⟨B, e⟩} {r : InS φ (⟨Ty.coprod A B, ⊥⟩::Γ) ⟨C, e⟩}
-  : let1 (inr a) r ≈ (let1 a $ let1 (inr (var 0 (by simp))) $ r.wk1)
-  := Uniform.rel $ TStep.rewrite InS.coe_wf InS.coe_wf (by constructor)
-
 theorem InS.let1_case {Γ : Ctx α ε} {a : InS φ Γ ⟨Ty.coprod A B, e⟩}
   {l : InS φ (⟨A, ⊥⟩::Γ) ⟨C, e⟩} {r : InS φ (⟨B, ⊥⟩::Γ) ⟨C, e⟩}
   {s : InS φ (⟨C, ⊥⟩::Γ) ⟨D, e⟩}
diff --git a/DeBruijnSSA/BinSyntax/Syntax/Compose/Term.lean b/DeBruijnSSA/BinSyntax/Syntax/Compose/Term.lean
index 36ab67b..ed914fa 100644
--- a/DeBruijnSSA/BinSyntax/Syntax/Compose/Term.lean
+++ b/DeBruijnSSA/BinSyntax/Syntax/Compose/Term.lean
@@ -1,5 +1,4 @@
 import DeBruijnSSA.BinSyntax.Syntax.Subst
-import DeBruijnSSA.BinSyntax.Syntax.Rewrite
 import DeBruijnSSA.InstSet
 
 namespace BinSyntax
diff --git a/DeBruijnSSA/BinSyntax/Syntax/Rewrite.lean b/DeBruijnSSA/BinSyntax/Syntax/Rewrite.lean
deleted file mode 100644
index c7396f8..0000000
--- a/DeBruijnSSA/BinSyntax/Syntax/Rewrite.lean
+++ /dev/null
@@ -1,132 +0,0 @@
-namespace BinSyntax
-namespace Region
-
--- inductive PureBeta (Γ : ℕ → ε) : Region φ → Region φ → Prop
---   | let1 (e : Term φ) (r : Region φ)
---     : e.effect Γ = ⊥ → PureBeta Γ (r.let1 e) (r.vsubst e.subst0)
-
--- theorem PureBeta.let1_pure {Γ : ℕ → ε} {e} {r r' : Region φ}
---   (h : PureBeta Γ (r.let1 e) r') : e.effect Γ = ⊥ := by cases h; assumption
-
--- theorem PureBeta.let1_trg {Γ : ℕ → ε} {e} {r r' : Region φ}
---   (h : PureBeta Γ (r.let1 e) r') : r' = r.vsubst e.subst0 := by cases h; rfl
-
--- inductive Reduce : Region φ → Region φ → Prop
---   | let2_pair (a b r) : Reduce (let2 (Term.pair a b) r) (let1 a $ let1 (b.wk Nat.succ) $ r)
---   | case_inl (e r s) : Reduce (case (Term.inl e) r s) (let1 e r)
---   | case_inr (e r s) : Reduce (case (Term.inr e) r s) (let1 e s)
-
--- theorem Reduce.let2_pair_trg {a b} {r r' : Region φ}
---   (h : Reduce (let2 (Term.pair a b) r) r')
---   : r' = (let1 a $ let1 (b.wk Nat.succ) $ r) := by cases h; rfl
-
--- theorem Reduce.case_inl_trg {e} {r s r' : Region φ}
---   (h : Reduce (case (Term.inl e) r s) r')
---   : r' = (let1 e r) := by cases h; rfl
-
--- theorem Reduce.case_inr_trg {e} {r s s' : Region φ}
---   (h : Reduce (case (Term.inr e) r s) s')
---   : s' = (let1 e s) := by cases h; rfl
-
--- inductive TermEta1 : Region φ → Region φ → Prop
---   | let1_op (f e r) : TermEta1 (let1 (Term.op f e) r)
---     (let1 e
---       $ let1 (Term.op f (Term.var 0))
---       $ r.vwk (Nat.liftWk Nat.succ))
---   | let1_pair (a b r) : TermEta1 (let1 (Term.pair a b) r)
---     (let1 a
---       $ let1 (b.wk Nat.succ)
---       $ let1 (Term.pair (Term.var 1) (Term.var 0))
---       $ r.vwk (Nat.liftWk (· + 2))
---     )
---   | let1_inl (e r) : TermEta1 (let1 (Term.inl e) r)
---     (let1 e
---       $ let1 (Term.inl (Term.var 0))
---       $ r.vwk (Nat.liftWk Nat.succ))
---   | let1_inr (e r) : TermEta1 (let1 (Term.inr e) r)
---     (let1 e
---       $ let1 (Term.inr (Term.var 0))
---       $ r.vwk (Nat.liftWk Nat.succ))
---   | let1_abort (e r) : TermEta1 (let1 (Term.abort e) r)
---     (let1 e
---       $ let1 (Term.abort (Term.var 0))
---       $ r.vwk (Nat.liftWk Nat.succ))
-
--- theorem TermEta1.let1_op_trg {f e} {r r' : Region φ}
---   (h : TermEta1 (let1 (Term.op f e) r) r')
---   : r' = (let1 e $ let1 (Term.op f (Term.var 0)) $ r.vwk (Nat.liftWk Nat.succ))
---   := by cases h; rfl
-
--- theorem TermEta1.let1_pair_trg {a b} {r r' : Region φ}
---   (h : TermEta1 (let1 (Term.pair a b) r) r')
---   : r' = (let1 a
---     $ let1 (b.wk Nat.succ)
---     $ let1 (Term.pair (Term.var 1) (Term.var 0))
---     $ r.vwk (Nat.liftWk (· + 2)))
---   := by cases h; rfl
-
--- theorem TermEta1.let1_inl_trg {e} {r r' : Region φ}
---   (h : TermEta1 (let1 (Term.inl e) r) r')
---   : r' = (let1 e $ let1 (Term.inl (Term.var 0)) $ r.vwk (Nat.liftWk Nat.succ))
---   := by cases h; rfl
-
--- theorem TermEta1.let1_inr_trg {e} {r r' : Region φ}
---   (h : TermEta1 (let1 (Term.inr e) r) r')
---   : r' = (let1 e $ let1 (Term.inr (Term.var 0)) $ r.vwk (Nat.liftWk Nat.succ))
---   := by cases h; rfl
-
--- theorem TermEta1.let1_abort_trg {e} {r r' : Region φ}
---   (h : TermEta1 (let1 (Term.abort e) r) r')
---   : r' = (let1 e $ let1 (Term.abort (Term.var 0)) $ r.vwk (Nat.liftWk Nat.succ))
---   := by cases h; rfl
-
--- inductive TermEta2 : Region φ → Region φ → Prop
---   | let2_op (f e r) : TermEta2 (let2 (Term.op f e) r) (let1 e
---       $ let2 (Term.op f (Term.var 0))
---       $ r.vwk (Nat.liftnWk 2 Nat.succ))
---   | let2_abort (e r) : TermEta2 (let2 (Term.abort e) r) (let1 e
---       $ let2 (Term.abort (Term.var 0))
---       $ r.vwk (Nat.liftnWk 2 Nat.succ))
-
--- inductive Eta : Region φ → Region φ → Prop
---   | let1_case (a b r s) : Eta
---     (let1 a $ case (b.wk Nat.succ) r s)
---     (case b (let1 (a.wk Nat.succ) r) (let1 (a.wk Nat.succ) s))
---   | let2_case (a b r s) : Eta
---     (let2 a $ case (b.wk (· + 2)) r s)
---     (case b (let2 (a.wk Nat.succ) r) (let2 (a.wk Nat.succ) s))
---   | cfg_br_lt (ℓ e n G) (h : ℓ < n) : Eta
---     (cfg (br ℓ e) n G)
---     (cfg ((G ⟨ℓ, h⟩).vsubst e.subst0) n G)
---   | cfg_br_ge (ℓ e n G) (h : n ≤ ℓ) : Eta
---     (cfg (br ℓ e) n G)
---     (br (ℓ - n) e)
---   | cfg_let1 (a β n G) : Eta
---     (cfg (let1 a β) n G)
---     (let1 a $ cfg β n (vwk Nat.succ ∘ G))
---   | cfg_let2 (a β n G) : Eta
---     (cfg (let2 a β) n G)
---     (let2 a $ cfg β n (vwk (· + 2) ∘ G))
---   | cfg_case (e r s n G) : Eta
---     (cfg (case e r s) n G)
---     (case e (cfg r n (vwk Nat.succ ∘ G)) (cfg s n (vwk Nat.succ ∘ G)))
---   | cfg_cfg (β n G n' G') : Eta
---     (cfg (cfg β n G) n' G')
---     (cfg β (n + n') (Fin.addCases G (lwk (· + n) ∘ G')))
-
--- inductive SimpleCongruence (P : Region φ → Region φ → Prop) : Region φ → Region φ → Prop
---   | step (r r') : P r r' → SimpleCongruence P r r'
---   | let1 (e r r') : SimpleCongruence P r r' → SimpleCongruence P (let1 e r) (let1 e r')
---   | let2 (e r r') : SimpleCongruence P r r' → SimpleCongruence P (let2 e r) (let2 e r')
---   | case_left (e r s r') : SimpleCongruence P r r' → SimpleCongruence P (case e r s) (case e r' s)
---   | case_right (e r s s') : SimpleCongruence P s s' → SimpleCongruence P (case e r s) (case e r s')
---   | cfg_entry (r r' n G) : SimpleCongruence P r r' → SimpleCongruence P (cfg r n G) (cfg r' n G)
---   | cfg_block (r r' n G i G') : SimpleCongruence P r r' → G' = Function.update G i r' →
---     SimpleCongruence P (cfg β n G) (cfg β n G')
-
--- theorem SimpleCongruence.refl (hP : IsRefl _ P) (r : Region φ) : SimpleCongruence P r r :=
---   step _ _ (hP.refl r)
-
-end Region
-
-end BinSyntax
diff --git a/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Region/Directed.lean b/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Region/Directed.lean
deleted file mode 100644
index 7e5a2ab..0000000
--- a/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Region/Directed.lean
+++ /dev/null
@@ -1,376 +0,0 @@
-import Mathlib.Combinatorics.Quiver.Path
-import Mathlib.Combinatorics.Quiver.Symmetric
-import Mathlib.CategoryTheory.PathCategory
-import Mathlib.Algebra.Order.BigOperators.Group.Finset
-
-import Discretion.Correspondence.Definitions
-
-import DeBruijnSSA.BinSyntax.Syntax.Subst
-import DeBruijnSSA.BinSyntax.Syntax.Effect.Subst
-import DeBruijnSSA.BinSyntax.Syntax.Fv
-
-import DeBruijnSSA.BinSyntax.Syntax.Rewrite.Region.Rewrite
-import DeBruijnSSA.BinSyntax.Syntax.Rewrite.Region.Equiv
-import DeBruijnSSA.BinSyntax.Syntax.Rewrite.Region.Reduce
-import DeBruijnSSA.BinSyntax.Syntax.Rewrite.Region.Step
-
-import DeBruijnSSA.BinSyntax.Syntax.Rewrite.Region.Cong
-
-namespace BinSyntax
-
-variable {φ : Type u} {ε : Type v} [Φ: EffectSet φ ε] [SemilatticeSup ε] [OrderBot ε]
-
--- -- TODO: define as Subst.cons or smt...
--- def Term.subst₂ (a b: Term φ) : Subst φ
---   | 0 => a
---   | 1 => b
---   | n + 2 => Term.var n
-
-namespace Region
-
-open Term
-
-abbrev RWD (P : (ℕ → ε) → Region φ → Region φ → Type _) (Γ : ℕ → ε) := Corr.Path ((BCongD P) Γ)
-
--- TODO: RwD is effect monotone/antitone iff underlying is
--- ==> RwD is effect preserving iff underlying is
-
-@[match_pattern]
-def RWD.refl {P} {Γ : ℕ → ε} (r : Region φ) : RWD P Γ r r := Corr.Path.nil r
-
-@[match_pattern]
-def RWD.cons {P} {Γ : ℕ → ε} {a b c : Region φ} : RWD P Γ a b → BCongD P Γ b c → RWD P Γ a c
-  := Corr.Path.cons
-
-def RWD.single {P} {Γ : ℕ → ε} {a b : Region φ} : BCongD P Γ a b → RWD P Γ a b := Corr.Path.single
-
-def RWD.comp {P} {Γ : ℕ → ε} {a b c : Region φ} : RWD P Γ a b → RWD P Γ b c → RWD P Γ a c
-  := Corr.Path.comp
-
-def RWD.let1_beta {Γ : ℕ → ε} (e) (r : Region φ) (h : e.effect Γ = ⊥)
-  : RWD StepD Γ (let1 e r) (r.vsubst e.subst0)
-  := single $ BCongD.rel $ StepD.let1_beta e r h
-
-def RWD.case_inl {Γ : ℕ → ε} (e) (r s : Region φ)
-  : RWD StepD Γ (case (inl e) r s) (let1 e r)
-  := single $ BCongD.rel $ StepD.case_inl e r s
-
-def RWD.case_inr {Γ : ℕ → ε} (e) (r s : Region φ)
-  : RWD StepD Γ (case (inr e) r s) (let1 e s)
-  := single $ BCongD.rel $ StepD.case_inr e r s
-
-def RWD.let1_op {Γ : ℕ → ε} (f e) (r : Region φ)
-  : RWD StepD Γ (let1 (op f e) r) (let1 e $ let1 (op f (var 0)) $ r.vwk (Nat.liftWk Nat.succ))
-  := single $ BCongD.rel $ StepD.let1_op f e r
-
-def RWD.let1_op_op {Γ : ℕ → ε} (f e) (r : Region φ)
-  : RWD StepD Γ (let1 e $ let1 (op f (var 0)) $ r.vwk (Nat.liftWk Nat.succ))
-    (let1 (op f e) r)
-  := single $ BCongD.rel $ StepD.let1_op_op f e r
-
-def RWD.let1_pair {Γ : ℕ → ε} (a b) (r : Region φ)
-  : RWD StepD Γ (let1 (pair a b) r)
-    (let1 a $ let1 (b.wk Nat.succ) $ let1 (pair (var 1) (var 0)) r.vwk1.vwk1
-  )
-  := single $ BCongD.rel $ StepD.let1_pair a b r
-
-def RWD.let1_pair_op {Γ : ℕ → ε} (a b) (r : Region φ)
-  : RWD StepD Γ (let1 a $ let1 (b.wk Nat.succ) $ let1 (pair (var 1) (var 0)) r.vwk1.vwk1)
-    (let1 (pair a b) r)
-  := single $ BCongD.rel $ StepD.let1_pair_op a b r
-
-def RWD.let1_inl {Γ : ℕ → ε} (e) (r : Region φ)
-  : RWD StepD Γ (let1 (inl e) r) (let1 e $ let1 (inl (var 0)) $ r.vwk (Nat.liftWk Nat.succ))
-  := single $ BCongD.rel $ StepD.let1_inl e r
-
-def RWD.let1_inl_op {Γ : ℕ → ε} (e) (r : Region φ)
-  : RWD StepD Γ (let1 e $ let1 (inl (var 0)) $ r.vwk (Nat.liftWk Nat.succ))
-    (let1 (inl e) r)
-  := single $ BCongD.rel $ StepD.let1_inl_op e r
-
-def RWD.let1_inr {Γ : ℕ → ε} (e) (r : Region φ)
-  : RWD StepD Γ (let1 (inr e) r) (let1 e $ let1 (inr (var 0)) $ r.vwk (Nat.liftWk Nat.succ))
-  := single $ BCongD.rel $ StepD.let1_inr e r
-
-def RWD.let1_inr_op {Γ : ℕ → ε} (e) (r : Region φ)
-  : RWD StepD Γ (let1 e $ let1 (inr (var 0)) $ r.vwk (Nat.liftWk Nat.succ))
-    (let1 (inr e) r)
-  := single $ BCongD.rel $ StepD.let1_inr_op e r
-
-def RWD.let1_abort {Γ : ℕ → ε} (e) (r : Region φ)
-  : RWD StepD Γ (let1 (abort e) r) (let1 e $ let1 (abort (var 0)) $ r.vwk (Nat.liftWk Nat.succ))
-  := single $ BCongD.rel $ StepD.let1_abort e r
-
-def RWD.let1_abort_op {Γ : ℕ → ε} (e) (r : Region φ)
-  : RWD StepD Γ (let1 e $ let1 (abort (var 0)) $ r.vwk (Nat.liftWk Nat.succ))
-    (let1 (abort e) r)
-  := single $ BCongD.rel $ StepD.let1_abort_op e r
-
-def RWD.cfg_br_lt {Γ : ℕ → ε} (ℓ) (e : Term φ) (n G) (h : ℓ < n)
-  : RWD StepD Γ (cfg (br ℓ e) n G) (cfg ((G ⟨ℓ, h⟩).let1 e) n G)
-  := single $ BCongD.rel $ StepD.cfg_br_lt ℓ e n G h
-
-def RWD.cfg_br_lt_op {Γ : ℕ → ε} (ℓ) (e : Term φ) (n G) (h : ℓ < n)
-  : RWD StepD Γ (cfg ((G ⟨ℓ, h⟩).let1 e) n G) (cfg (br ℓ e) n G)
-  := single $ BCongD.rel $ StepD.cfg_br_lt_op ℓ e n G h
-
--- def RWD.cfg_let1 {Γ : ℕ → ε} (a : Term φ) (β n G)
---   : RWD StepD Γ (cfg (let1 a β) n G) (let1 a $ cfg β n (vwk1 ∘ G))
---   := single $ BCongD.rel $ StepD.cfg_let1 a β n G
-
--- def RWD.cfg_let1_op {Γ : ℕ → ε} (a : Term φ) (β n G)
---   : RWD StepD Γ (let1 a $ cfg β n (vwk1 ∘ G))
---     (cfg (let1 a β) n G)
---   := single $ BCongD.rel $ StepD.cfg_let1_op a β n G
-
--- def RWD.cfg_let2 {Γ : ℕ → ε} (a : Term φ) (β n G)
---   : RWD StepD Γ (cfg (let2 a β) n G) (let2 a $ cfg β n (vwk1 ∘ vwk1 ∘ G))
---   := single $ BCongD.rel $ StepD.cfg_let2 a β n G
-
--- def RWD.cfg_let2_op {Γ : ℕ → ε} (a : Term φ) (β n G)
---   : RWD StepD Γ (let2 a $ cfg β n (vwk1 ∘ vwk1 ∘ G))
---     (cfg (let2 a β) n G)
---   := single $ BCongD.rel $ StepD.cfg_let2_op a β n G
-
--- def RWD.cfg_case {Γ : ℕ → ε} (e : Term φ) (r s n G)
---   : RWD StepD Γ (cfg (case e r s) n G)
---     (case e (cfg r n (vwk1 ∘ G)) (cfg s n (vwk1 ∘ G))
---   )
---   := single $ BCongD.rel $ StepD.cfg_case e r s n G
-
--- def RWD.cfg_case_op {Γ : ℕ → ε} (e : Term φ) (r s n G)
---   : RWD StepD Γ (case e (cfg r n (vwk1 ∘ G)) (cfg s n (vwk1 ∘ G)))
---     (cfg (case e r s) n G)
---   := single $ BCongD.rel $ StepD.cfg_case_op e r s n G
-
--- def RWD.cfg_cfg {Γ : ℕ → ε} (β : Region φ) (n G n' G')
---   : RWD StepD Γ (cfg (cfg β n G) n' G') (cfg β (n + n') (Fin.addCases G (lwk (· + n) ∘ G')))
---   := single $ BCongD.rel $ StepD.cfg_cfg β n G n' G'
-
--- def RWD.cfg_cfg_op {Γ : ℕ → ε} (β : Region φ) (n G n' G')
---   : RWD StepD Γ (cfg β (n + n') (Fin.addCases G (lwk (· + n) ∘ G')))
---     (cfg (cfg β n G) n' G')
---   := single $ BCongD.rel $ StepD.cfg_cfg_op β n G n' G'
-
--- def RWD.cfg_zero {Γ : ℕ → ε} (β : Region φ) (G)
---   : RWD StepD Γ (cfg β 0 G) β := single $ BCongD.rel $ StepD.cfg_zero β G
-
--- def RWD.cfg_zero_op {Γ : ℕ → ε} (β : Region φ) (G)
---   : RWD StepD Γ β (cfg β 0 G) := single $ BCongD.rel $ StepD.cfg_zero_op β G
-
--- def RWD.wk_cfg {Γ : ℕ → ε} (β : Region φ) (n G k) (ρ : Fin k → Fin n) /-(hρ : Function.Bijective ρ)-/
---   : RWD StepD Γ
---     (cfg (lwk (Fin.toNatWk ρ) β) n (lwk (Fin.toNatWk ρ) ∘ G))
---     (cfg β k (G ∘ ρ))
---   := single $ BCongD.rel $ StepD.wk_cfg β n G k ρ
-
--- def RWD.dead_cfg_left {Γ : ℕ → ε} (β : Region φ) (n G m G')
---   : RWD StepD Γ
---     (cfg (β.lwk (· + n)) (n + m) (Fin.addCases G (lwk (· + n) ∘ G')))
---     (cfg β m G')
---   := single $ BCongD.rel $ StepD.dead_cfg_left β n G m G'
-
--- def RWD.swap_cfg' {Γ : ℕ → ε} (β : Region φ) (n G m G')
---   : RWD StepD Γ
---     (cfg
---       (lwk (Fin.toNatWk (Fin.swapAdd n m)) β)
---       (m + n) (lwk (Fin.toNatWk (Fin.swapAdd n m)) ∘ Fin.addCases G' G))
---     (cfg β (n + m) (Fin.addCases G G'))
---   :=
---   have h : Fin.addCases G G' = Fin.addCases G' G ∘ Fin.swapAdd n m := by
---     rw [Fin.addCases_comp_swapAdd]
---   by
---     rw [h]
---     apply wk_cfg
-
-def RWD.cast_trg {P} {Γ : ℕ → ε} {r₀ r₁ r₁' : Region φ} (h : RWD P Γ r₀ r₁) (hr₁ : r₁ = r₁')
-  : RWD P Γ r₀ r₁'
-  := Corr.Path.cast_trg h hr₁
-
-def RWD.cast_src {P} {Γ : ℕ → ε} {r₀ r₀' r₁ : Region φ} (hr₀ : r₀ = r₀') (h : RWD P Γ r₀' r₁)
-  : RWD P Γ r₀ r₁
-  := Corr.Path.cast_src hr₀ h
-
-def RWD.cast {P} {Γ : ℕ → ε} {r₀ r₀' r₁ r₁' : Region φ} (hr₀ : r₀ = r₀') (hr₁ : r₁ = r₁')
-  (h : RWD P Γ r₀ r₁) : RWD P Γ r₀' r₁'
-  := Corr.Path.cast hr₀ hr₁ h
-
--- def RWD.swap_cfg {Γ : ℕ → ε} (β : Region φ) (n G m G')
---   : RWD StepD Γ
---     (cfg β (n + m) (Fin.addCases G G'))
---     (cfg
---       (lwk (Fin.toNatWk (Fin.swapAdd n m)) β)
---       (m + n) (lwk (Fin.toNatWk (Fin.swapAdd n m)) ∘ Fin.addCases G' G))
---   := cast_trg (cast_src
---     (by
---       rw [
---         <-Fin.comp_addCases,
---         <-Function.comp_assoc,
---         lwk_lwk, comp_lwk,
---         Fin.swapAdd
---       ]
---       simp [<-Fin.toNatWk_comp, Fin.addCases_natAdd_castAdd_nil]
---     )
---     (swap_cfg'
---       (β.lwk (Fin.toNatWk (Fin.addCases (Fin.natAdd m) (Fin.castAdd n))))
---       m
---       (lwk (Fin.toNatWk (Fin.addCases (Fin.natAdd m) (Fin.castAdd n))) ∘ G')
---       n
---       (lwk (Fin.toNatWk (Fin.addCases (Fin.natAdd m) (Fin.castAdd n))) ∘ G)))
---     (by simp [Fin.comp_addCases, Fin.swapAdd])
-
-def RWD.let1V0_id {Γ : ℕ → ε} (r : Region φ) (hΓ : Γ 0 = ⊥)
-  : RWD StepD Γ r.let1V0 r
-  := cast_trg
-    (let1_beta (Term.var 0) (r.vwk (Nat.liftWk Nat.succ)) hΓ)
-    (by rw [<-vsubst_fromWk_apply, vsubst_vsubst, vsubst_id']; funext i; cases i <;> rfl)
-
-def RWD.let2_eta {Γ : ℕ → ε} (r : Region φ)
-  : RWD StepD Γ
-    (let2 e $
-     let1 ((Term.var 1).pair (Term.var 0)) $
-     r.vwk1.vwk1) (let1 e r)
-  := single $ BCongD.rel $ StepD.let2_eta e r
-
-def RWD.let2_eta_op {Γ : ℕ → ε} (r : Region φ)
-  : RWD StepD Γ (let1 (Term.var 0) r)
-    (let2 (Term.var 0) $
-     let1 ((Term.var 1).pair (Term.var 0)) $
-     r.vwk1.vwk1)
-  := single $ BCongD.rel $ StepD.let2_eta_op r
-
--- def RWD.let1_eta {Γ : ℕ → ε} (r : Region φ)
---   : RWD StepD Γ
---     (let1 (Term.var 0) $
---      r.vwk1) r
---   := single $ BCongD.rel $ StepD.let1_eta r
-
--- def RWD.let1_eta_op {Γ : ℕ → ε} (r : Region φ)
---   : RWD StepD Γ r
---     (let1 (Term.var 0) $
---      r.vwk1)
---   := single $ BCongD.rel $ StepD.let1_eta_op r
-
-instance instTransRWD
-  {P : (ℕ → ε) → Region φ → Region φ → Type _} {Γ}
-  : Trans (RWD P Γ) (RWD P Γ) (RWD P Γ) where
-  trans := RWD.comp
-
--- infixr:10 " ⟶R " => λ{P Γ} => RWD P Γ
-
-def RWD.let1 {P} {Γ : ℕ → ε} {r r'} (e : Term φ) (h : RWD P (Nat.liftBot Γ) r r')
-  : RWD P Γ (let1 e r) (let1 e r')
-  := (BCongD.let1_func e).mapPath h
-
-def RWD.let2 {P} {Γ : ℕ → ε} {r r'} (e : Term φ) (h : RWD P (Nat.liftnBot 2 Γ) r r')
-  : RWD P Γ (let2 e r) (let2 e r')
-  := (BCongD.let2_func e).mapPath h
-
-def RWD.case_left {P} {Γ : ℕ → ε} {r r'} (e : Term φ) (h : RWD P (Nat.liftBot Γ) r r') (s)
-  : RWD P Γ (case e r s) (case e r' s)
-  := (BCongD.case_left_func e s).mapPath h
-
-def RWD.case_right {P} {Γ : ℕ → ε} (e : Term φ) (r) (h : RWD P (Nat.liftBot Γ) s s')
-  : RWD P Γ (case e r s) (case e r s')
-  := (BCongD.case_right_func e r).mapPath h
-
-def RWD.cfg_entry {P} {Γ : ℕ → ε} {r r' : Region φ} (h : RWD P Γ r r') (n G)
-  : RWD P Γ (cfg r n G) (cfg r' n G)
-  := (BCongD.cfg_entry_func n G).mapPath h
-
-def RWD.cfg_block' {P} {Γ : ℕ → ε} {r r' : Region φ} (β n G i) (h : RWD P (Nat.liftBot Γ) r r')
-  : RWD P Γ (cfg β n (Function.update G i r)) (cfg β n (Function.update G i r'))
-  := (BCongD.cfg_block_func' β n G i).mapPath h
-
-def RWD.case {P} {Γ : ℕ → ε} {r r' : Region φ} (e : Term φ)
-  (hr : RWD P (Nat.liftBot Γ) r r')
-  (hs : RWD P (Nat.liftBot Γ) s s')
-  : RWD P Γ (case e r s) (case e r' s')
-  := (case_left e hr s).comp (case_right e r' hs)
-
-def RWD.of_eq {P} {Γ : ℕ → ε} {r r' : Region φ} (h : r = r')
-  : RWD P Γ r r' := cast_trg (refl r) h
-
-def RWD.cfg_blocks_partial {P} {Γ : ℕ → ε} (β n) (G : Fin n → Region φ) (G': Fin n → Region φ)
-  (h : ∀i, RWD P (Nat.liftBot Γ) (G i) (G' i))
-  : ∀k : ℕ, RWD P Γ (Region.cfg β n G) (Region.cfg β n (λi => if i < k then G' i else G i))
-  | 0 => RWD.refl _
-  | k + 1 => if hk : k < n then
-      RWD.comp
-        (cast_trg (cfg_blocks_partial β n G G' h k)
-          (by
-            congr
-            rw [Function.eq_update_self_iff]
-            simp))
-        (cast_trg (cfg_block' β n
-          (λi => if i < k then G' i else G i)
-          ⟨k, hk⟩ (h ⟨k, hk⟩))
-          (by
-            congr
-            funext i
-            split
-            case _ h =>
-              rw [Function.update_apply]
-              split
-              case _ h =>
-                cases h
-                rfl
-              case _ he =>
-                have h : i < k := Nat.lt_of_le_of_ne
-                  (Nat.le_of_lt_succ h)
-                  (Fin.val_ne_of_ne he)
-                simp [h]
-            case _ h =>
-              have h := Nat.le_of_not_lt h
-              rw [Function.update_noteq, ite_cond_eq_false]
-              simp [Nat.le_of_succ_le h]
-              apply Fin.ne_of_gt
-              exact Nat.lt_of_succ_le h
-            ))
-    else
-      cast_trg (cfg_blocks_partial β n G G' h k) (by
-        have hk := Nat.le_of_not_lt hk;
-        simp only [cfg.injEq, heq_eq_eq, true_and]
-        funext i
-        have hi := Nat.lt_of_lt_of_le i.prop hk
-        simp [hi, Nat.lt_succ_of_lt hi]
-      )
-
-def RWD.cfg_blocks {P} {Γ : ℕ → ε} (β n) (G G' : Fin n → Region φ)
-  (h : ∀i, RWD P (Nat.liftBot Γ) (G i) (G' i))
-  : RWD P Γ (Region.cfg β n G) (Region.cfg β n G')
-  := cast_trg (cfg_blocks_partial β n G G' h n) (by simp)
-
--- def RWD.dead_cfg_right {Γ : ℕ → ε} (β : Region φ) (n G m G')
---   : RWD StepD Γ
---     (cfg (β.lwk (n.liftnWk (· + m))) (n + m) (Fin.addCases (lwk (n.liftnWk (· + m)) ∘ G) G'))
---     (cfg β n G) :=
---     (cast_trg (swap_cfg (β.lwk (n.liftnWk (· + m))) n (lwk (n.liftnWk (· + m)) ∘ G) m G')
---       (by rw [
---         Fin.comp_addCases, lwk_lwk, <-Function.comp_assoc, comp_lwk,
---         Fin.toNatWk_swapAdd_comp_liftnWk_add]
---       )).comp
---     (dead_cfg_left β m _ n G)
-
--- def RWD.cfg_elim {Γ : ℕ → ε} (β : Region φ) (n G)
---   : RWD StepD Γ (cfg (β.lwk (· + n)) n G) β
---   :=
---   let s : RWD StepD Γ
---     (cfg (β.lwk (· + n)) n G)
---     (cfg (β.lwk (· + n)) (n + 0) (Fin.addCases G (lwk (· + n) ∘ Fin.elim0)))
---     := RWD.of_eq (by simp [Fin.addCases_zero])
---   (s.comp (dead_cfg_left β n G 0 Fin.elim0)).comp (RWD.cfg_zero _ _)
-  -- := match β with
-  -- | Region.br ℓ e => (cfg_br_ge (ℓ + n) e n G (by simp)).cast_trg (by simp)
-  -- | Region.let1 a β => (cfg_let1 a (β.lwk (· + n)) n G).comp (let1 a (cfg_elim β n _))
-  -- | Region.let2 a β => (cfg_let2 a (β.lwk (· + n)) n G).comp (let2 a (cfg_elim β n _))
-  -- | Region.case e r s =>
-  --   (cfg_case e (r.lwk (· + n)) (s.lwk (· + n)) n G).comp
-  --     (case e (cfg_elim r n _) (cfg_elim s n _))
-  -- | Region.cfg β n' G' => (cfg_cfg _ _ _ _ _).comp (dead_cfg_right _ _ _ _ _)
-
--- def RWD.cfg_br_ge {Γ : ℕ → ε} (ℓ) (e : Term φ) (n G) (h : n ≤ ℓ)
---   : RWD StepD Γ (cfg (br ℓ e) n G) (br (ℓ - n) e)
---   := cast_src (by simp [h]) (cfg_elim (br (ℓ - n) e) n G)
-
--- TODO: vwk, lwk lore...
diff --git a/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Region/Equiv.lean b/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Region/Equiv.lean
index d8f6175..c77b826 100644
--- a/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Region/Equiv.lean
+++ b/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Region/Equiv.lean
@@ -79,9 +79,6 @@ theorem eqv_let1_inl {e r} : @let1 φ (inl e) r ≈ (let1 e $ let1 (inl (var 0))
 theorem eqv_let1_inr {e r} : @let1 φ (inr e) r ≈ (let1 e $ let1 (inr (var 0)) $ r.vwk1)
   := Relation.EqvGen.rel _ _ $ Cong.rel $ Rewrite.let1_inr e r
 
-theorem eqv_let1_abort {e r} : @let1 φ (abort e) r ≈ (let1 e $ let1 (abort (var 0)) $ r.vwk1)
-  := Relation.EqvGen.rel _ _ $ Cong.rel $ Rewrite.let1_abort e r
-
 theorem eqv_let2_bind {e r} : @let2 φ e r ≈ (let1 e $ let2 (var 0) $ r.vwk (Nat.liftnWk 2 Nat.succ))
   := Relation.EqvGen.rel _ _ $ Cong.rel $ Rewrite.let2_bind e r
 
diff --git a/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Region/Rewrite.lean b/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Region/Rewrite.lean
index c8417e8..05d8658 100644
--- a/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Region/Rewrite.lean
+++ b/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Region/Rewrite.lean
@@ -22,10 +22,6 @@ inductive RewriteD : Region φ → Region φ → Type _
     RewriteD (let1 (Term.let1 a b) r) (let1 a $ let1 b $ r.vwk1)
   | let1_let2 (a b r) :
     RewriteD (let1 (Term.let2 a b) r) (let2 a $ let1 b $ r.vwk1.vwk1)
-  | let1_inl (e r) :
-    RewriteD (let1 (inl e) r) (let1 e $ let1 (inl (var 0)) $ r.vwk1)
-  | let1_inr (e r) :
-    RewriteD (let1 (inr e) r) (let1 e $ let1 (inr (var 0)) $ r.vwk1)
   | let1_case (a l r s) :
     RewriteD (let1 (Term.case a l r) s) (case a (let1 l $ s.vwk1) (let1 r $ s.vwk1))
   | let1_abort (e r) :
@@ -150,10 +146,6 @@ inductive Rewrite : Region φ → Region φ → Prop
     Rewrite (let1 (Term.let1 a b) r) (let1 a $ let1 b $ r.vwk1)
   | let1_let2 (a b r) :
     Rewrite (let1 (Term.let2 a b) r) (let2 a $ let1 b $ r.vwk1.vwk1)
-  | let1_inl (e r) :
-    Rewrite (let1 (inl e) r) (let1 e $ let1 (inl (var 0)) $ r.vwk1)
-  | let1_inr (e r) :
-    Rewrite (let1 (inr e) r) (let1 e $ let1 (inr (var 0)) $ r.vwk1)
   | let1_case (a l r s) :
     Rewrite (let1 (Term.case a l r) s) (case a (let1 l $ s.vwk1) (let1 r $ s.vwk1))
   | let1_abort (e r) :
@@ -271,12 +263,6 @@ def RewriteD.vsubst {r r' : Region φ} (σ : Term.Subst φ) (p : RewriteD r r')
   | let1_let2 a b r =>
     convert (let1_let2 (a.subst σ) (b.subst (σ.liftn 2)) (r.vsubst σ.lift)) using 1
     simp [Term.subst, Region.vsubst_lift₂_vwk1, Term.Subst.liftn_two]
-  | let1_inl e r =>
-    convert (let1_inl (e.subst σ) (r.vsubst σ.lift)) using 1
-    simp [Term.subst, Region.vsubst_lift₂_vwk1]
-  | let1_inr e r =>
-    convert (let1_inr (e.subst σ) (r.vsubst σ.lift)) using 1
-    simp [Term.subst, Region.vsubst_lift₂_vwk1]
   | let1_case a l r s =>
     convert (let1_case (a.subst σ) (l.subst σ.lift) (r.subst σ.lift) (s.vsubst σ.lift)) using 1
     simp [Term.subst, Region.vsubst_lift₂_vwk1]
@@ -309,12 +295,6 @@ def RewriteD.lsubst {r r' : Region φ} (σ : Subst φ) (p : RewriteD r r')
   | let1_let2 a b r =>
     convert (let1_let2 a b (r.lsubst σ.vlift)) using 1
     simp [vwk1_lsubst_vlift, Subst.vliftn_two]
-  | let1_inl e r =>
-    convert (let1_inl e (r.lsubst σ.vlift)) using 1
-    simp [vwk1_lsubst_vlift]
-  | let1_inr e r =>
-    convert (let1_inr e (r.lsubst σ.vlift)) using 1
-    simp [vwk1_lsubst_vlift]
   | let1_case a l r s =>
     convert (let1_case a l r (s.lsubst σ.vlift)) using 1
     simp [vwk1_lsubst_vlift]
diff --git a/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Region/Step.lean b/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Region/Step.lean
deleted file mode 100644
index 500fdac..0000000
--- a/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Region/Step.lean
+++ /dev/null
@@ -1,240 +0,0 @@
-import Mathlib.Combinatorics.Quiver.Path
-import Mathlib.Combinatorics.Quiver.Symmetric
-import Mathlib.Algebra.Order.BigOperators.Group.Finset
-
-import Discretion.Correspondence.Definitions
-
-import DeBruijnSSA.BinSyntax.Syntax.Subst
-import DeBruijnSSA.BinSyntax.Syntax.Effect.Subst
-import DeBruijnSSA.BinSyntax.Syntax.Fv
-
-import DeBruijnSSA.BinSyntax.Syntax.Rewrite.Region.Rewrite
-import DeBruijnSSA.BinSyntax.Syntax.Rewrite.Region.Equiv
-import DeBruijnSSA.BinSyntax.Syntax.Rewrite.Region.Reduce
-
-import DeBruijnSSA.BinSyntax.Syntax.Rewrite.Region.Cong
-
-namespace BinSyntax
-
-variable {φ : Type u} {ε : Type v} [Φ: EffectSet φ ε] [SemilatticeSup ε] [OrderBot ε]
-
--- -- TODO: define as Subst.cons or smt...
--- def Term.subst₂ (a b: Term φ) : Subst φ
---   | 0 => a
---   | 1 => b
---   | n + 2 => Term.var n
-
-namespace Region
-
-open Term
-
-inductive StepD (Γ : ℕ → ε) : Region φ → Region φ → Type _
-  | let1_beta (e r) : e.effect Γ = ⊥ → StepD Γ (let1 e r) (r.vsubst e.subst0)
-  | reduce {r r'} : ReduceD r r' → StepD Γ r r'
-  | rw {r r'} : RewriteD r r' → StepD Γ r r'
-  | rw_op {r r'} : RewriteD r r' → StepD Γ r' r
-
--- TODO: separate beta relation? Then step is just the inf...
-
-inductive Step (Γ : ℕ → ε) : Region φ → Region φ → Prop
-  | let1_beta (e r) : e.effect Γ = ⊥ → Step Γ (let1 e r) (r.vsubst e.subst0)
-  | reduce {r r'} : Reduce r r' → Step Γ r r'
-  | rw {r r'} : Rewrite r r' → Step Γ r r'
-  | rw_op {r r'} : Rewrite r r' → Step Γ r' r
-
-theorem StepD.step {Γ : ℕ → ε} {r r' : Region φ} : StepD Γ r r' → Step Γ r r'
-  | let1_beta e r he => Step.let1_beta e r he
-  | reduce p => Step.reduce p.reduce
-  | rw p => Step.rw p.rewrite
-  | rw_op p => Step.rw_op p.rewrite
-
-theorem Step.nonempty {Γ : ℕ → ε} {r r' : Region φ} : Step Γ r r' → Nonempty (StepD Γ r r')
-  | let1_beta e r he => ⟨StepD.let1_beta e r he⟩
-  | reduce p => let ⟨d⟩ := p.nonempty; ⟨StepD.reduce d⟩
-  | rw p => let ⟨d⟩ := p.nonempty; ⟨StepD.rw d⟩
-  | rw_op p => let ⟨d⟩ := p.nonempty; ⟨StepD.rw_op d⟩
-
-theorem Step.nonempty_iff {Γ : ℕ → ε} {r r' : Region φ} : Step Γ r r' ↔ Nonempty (StepD Γ r r')
-  := ⟨Step.nonempty, λ⟨d⟩ => d.step⟩
-
-def StepD.vwk {Γ : ℕ → ε} {r r' : Region φ} (ρ : ℕ → ℕ)
-  : StepD (Γ ∘ ρ) r r' → StepD Γ (r.vwk ρ) (r'.vwk ρ)
-  | let1_beta e r he => by
-    simp only [Region.vwk, vsubst_subst0_vwk]
-    apply let1_beta
-    rw [Term.effect_wk]
-    assumption
-  | reduce p => reduce $ p.vwk ρ
-  | rw p => rw $ p.vwk ρ
-  | rw_op p => rw_op $ p.vwk ρ
-
-theorem Step.vwk {Γ : ℕ → ε} {r r' : Region φ} (ρ : ℕ → ℕ) (p : Step (Γ ∘ ρ) r r')
-  : Step Γ (r.vwk ρ) (r'.vwk ρ) := let ⟨d⟩ := p.nonempty; (d.vwk ρ).step
-
-inductive FStepD (Γ : ℕ → ε) : Region φ → Region φ → Type _
-  | let1_beta (e r) : e.effect Γ = ⊥ → FStepD Γ (let1 e r) (r.vsubst e.subst0)
-  | reduce {r r'} : ReduceD r r' → FStepD Γ r r'
-  | rw {r r'} : RewriteD r r' → FStepD Γ r r'
-
-inductive FStep (Γ : ℕ → ε) : Region φ → Region φ → Prop
-  | let1_beta (e r) : e.effect Γ = ⊥ → FStep Γ (let1 e r) (r.vsubst e.subst0)
-  | reduce {r r'} : Reduce r r' → FStep Γ r r'
-  | rw {r r'} : Rewrite r r' → FStep Γ r r'
-
-theorem FStepD.step {Γ : ℕ → ε} {r r' : Region φ} : FStepD Γ r r' → FStep Γ r r'
-  | let1_beta e r he => FStep.let1_beta e r he
-  | reduce p => FStep.reduce p.reduce
-  | rw p => FStep.rw p.rewrite
-
-theorem FStep.nonempty {Γ : ℕ → ε} {r r' : Region φ} : FStep Γ r r' → Nonempty (FStepD Γ r r')
-  | let1_beta e r he => ⟨FStepD.let1_beta e r he⟩
-  | reduce p => let ⟨d⟩ := p.nonempty; ⟨FStepD.reduce d⟩
-  | rw p => let ⟨d⟩ := p.nonempty; ⟨FStepD.rw d⟩
-
-theorem FStep.nonempty_iff {Γ : ℕ → ε} {r r' : Region φ} : FStep Γ r r' ↔ Nonempty (FStepD Γ r r')
-  := ⟨FStep.nonempty, λ⟨d⟩ => d.step⟩
-
--- theorem FStep.fvs_le {Γ : ℕ → ε} {r r' : Region φ} (p : FStep Γ r r')
---   : r'.fvs ⊆ r.fvs := by cases p with
---   | let1_beta e r he => apply fvs_vsubst0_le
---   | reduce p => exact p.fvs_le
---   | rw p => rw [p.fvs_eq]
-
-def FStepD.vwk {Γ : ℕ → ε} {r r' : Region φ} (ρ : ℕ → ℕ)
-  : FStepD (Γ ∘ ρ) r r' → FStepD Γ (r.vwk ρ) (r'.vwk ρ)
-  | let1_beta e r he => by
-    simp only [Region.vwk, vsubst_subst0_vwk]
-    apply let1_beta
-    rw [Term.effect_wk]
-    assumption
-  | reduce p => reduce $ p.vwk ρ
-  | rw p => rw $ p.vwk ρ
-
-theorem FStep.vwk {Γ : ℕ → ε} {r r' : Region φ} (ρ : ℕ → ℕ) (p : FStep (Γ ∘ ρ) r r')
-  : FStep Γ (r.vwk ρ) (r'.vwk ρ) := let ⟨d⟩ := p.nonempty; (d.vwk ρ).step
-
-def FStepD.wk_eff {Γ Δ : ℕ → ε} {r r' : Region φ}
-  (h : ∀i ∈ r.fvs, Γ i ≤ Δ i) : FStepD Δ r r' → FStepD Γ r r'
-  | let1_beta e r he => let1_beta e r (by
-    have he' := e.effect_le (λi hi => h i (Or.inl hi));
-    rw [he] at he'
-    simp only [le_bot_iff] at he'
-    exact he')
-  | reduce p => reduce p
-  | rw p => rw p
-
-theorem FStep.wk_eff {Γ Δ : ℕ → ε} {r r' : Region φ}
-  (h : ∀i ∈ r.fvs, Γ i ≤ Δ i) (p : FStep Δ r r') : FStep Γ r r'
-  := let ⟨d⟩ := p.nonempty; (d.wk_eff h).step
-
-def FStepD.lwk {Γ : ℕ → ε} {r r' : Region φ} (ρ : ℕ → ℕ)
-  : FStepD Γ r r' → FStepD Γ (r.lwk ρ) (r'.lwk ρ)
-  | let1_beta e r he => by
-    rw [lwk_vsubst]
-    apply let1_beta
-    exact he
-  | reduce p => reduce $ p.lwk ρ
-  | rw p => rw $ p.lwk ρ
-
-theorem FStep.lwk {Γ : ℕ → ε} {r r' : Region φ} (ρ : ℕ → ℕ) (p : FStep Γ r r')
-  : FStep Γ (r.lwk ρ) (r'.lwk ρ) := let ⟨d⟩ := p.nonempty; (d.lwk ρ).step
-
-@[match_pattern]
-def StepD.case_inl {Γ : ℕ → ε} (e : Term φ) (r s)
-  : StepD Γ (case (inl e) r s) (let1 e r)
-  := StepD.reduce (ReduceD.case_inl e r s)
-
-@[match_pattern]
-def StepD.case_inr {Γ : ℕ → ε} (e : Term φ) (r s)
-  : StepD Γ (case (inr e) r s) (let1 e s)
-  := StepD.reduce (ReduceD.case_inr e r s)
-
--- @[match_pattern]
--- def StepD.wk_cfg {Γ : ℕ → ε} (β : Region φ) (n G k) (ρ : Fin k → Fin n)
---   : StepD Γ (cfg (lwk (Fin.toNatWk ρ) β) n (lwk (Fin.toNatWk ρ) ∘ G))
---     (cfg β k (G ∘ ρ))
---   := StepD.reduce (ReduceD.wk_cfg β n G k ρ)
-
--- @[match_pattern]
--- def StepD.dead_cfg_left {Γ : ℕ → ε} (β : Region φ) (n G m G')
---   : StepD Γ (cfg (β.lwk (· + n)) (n + m) (Fin.addCases G (lwk (· + n) ∘ G')))
---     (cfg β m G')
---   := StepD.reduce (ReduceD.dead_cfg_left β n G m G')
-
-@[match_pattern]
-def StepD.let1_op {Γ : ℕ → ε} (f e) (r : Region φ)
-  : StepD Γ (let1 (op f e) r) (let1 e $ let1 (op f (var 0)) $ r.vwk (Nat.liftWk Nat.succ))
-  := StepD.rw $ RewriteD.let1_op f e r
-
-@[match_pattern]
-def StepD.let1_op_op {Γ : ℕ → ε} (f e) (r : Region φ)
-  : StepD Γ (let1 e $ let1 (op f (var 0)) $ r.vwk (Nat.liftWk Nat.succ))
-    (let1 (op f e) r)
-  := StepD.rw_op $ RewriteD.let1_op f e r
-
-@[match_pattern]
-def StepD.let1_inl {Γ : ℕ → ε} (e) (r : Region φ)
-  : StepD Γ (let1 (inl e) r) (let1 e $ let1 (inl (var 0)) $ r.vwk (Nat.liftWk Nat.succ))
-  := StepD.rw $ RewriteD.let1_inl e r
-
-@[match_pattern]
-def StepD.let1_inl_op {Γ : ℕ → ε} (e) (r : Region φ)
-  : StepD Γ (let1 e $ let1 (inl (var 0)) $ r.vwk (Nat.liftWk Nat.succ))
-    (let1 (inl e) r)
-  := StepD.rw_op $ RewriteD.let1_inl e r
-
-@[match_pattern]
-def StepD.let1_inr {Γ : ℕ → ε} (e) (r : Region φ)
-  : StepD Γ (let1 (inr e) r) (let1 e $ let1 (inr (var 0)) $ r.vwk (Nat.liftWk Nat.succ))
-  := StepD.rw $ RewriteD.let1_inr e r
-
-@[match_pattern]
-def StepD.let1_inr_op {Γ : ℕ → ε} (e) (r : Region φ)
-  : StepD Γ (let1 e $ let1 (inr (var 0)) $ r.vwk (Nat.liftWk Nat.succ))
-    (let1 (inr e) r)
-  := StepD.rw_op $ RewriteD.let1_inr e r
-
-@[match_pattern]
-def StepD.let1_abort {Γ : ℕ → ε} (e) (r : Region φ)
-  : StepD Γ (let1 (abort e) r) (let1 e $ let1 (abort (var 0)) $ r.vwk (Nat.liftWk Nat.succ))
-  := StepD.rw $ RewriteD.let1_abort e r
-
-@[match_pattern]
-def StepD.let1_abort_op {Γ : ℕ → ε} (e) (r : Region φ)
-  : StepD Γ (let1 e $ let1 (abort (var 0)) $ r.vwk (Nat.liftWk Nat.succ))
-    (let1 (abort e) r)
-  := StepD.rw_op $ RewriteD.let1_abort e r
-
-@[match_pattern]
-def StepD.cfg_br_lt {Γ : ℕ → ε} (ℓ) (e : Term φ) (n G) (h : ℓ < n)
-  : StepD Γ (cfg (br ℓ e) n G) (cfg ((G ⟨ℓ, h⟩).let1 e) n G)
-  := StepD.rw $ RewriteD.cfg_br_lt ℓ e n G h
-
-@[match_pattern]
-def StepD.cfg_br_lt_op {Γ : ℕ → ε} (ℓ) (e : Term φ) (n G) (h : ℓ < n)
-  : StepD Γ (cfg ((G ⟨ℓ, h⟩).let1 e) n G) (cfg (br ℓ e) n G)
-  := StepD.rw_op $ RewriteD.cfg_br_lt ℓ e n G h
-
-def StepD.cast_trg {Γ : ℕ → ε} {r₀ r₁ r₁' : Region φ} (p : StepD Γ r₀ r₁) (h : r₁ = r₁')
-  : StepD Γ r₀ r₁' := h ▸ p
-
-def StepD.cast_src {Γ : ℕ → ε} {r₀ r₀' r₁ : Region φ} (h : r₀' = r₀) (p : StepD Γ r₀ r₁)
-  : StepD Γ r₀' r₁ := h ▸ p
-
-def StepD.cast {Γ : ℕ → ε} {r₀ r₀' r₁ r₁' : Region φ} (h₀ : r₀ = r₀') (h₁ : r₁ = r₁')
-  (p : StepD Γ r₀ r₁) : StepD Γ r₀' r₁' := h₁ ▸ h₀ ▸ p
-
--- theorem StepD.effect_le {Γ : ℕ → ε} {r r' : Region φ} (p : StepD Γ r r')
---   : r'.effect Γ ≤ r.effect Γ := by
---   cases p with
---   | let1_beta _ _ he =>
---     apply le_of_eq
---     simp only [effect_vsubst, Subst.effect, effect, he, ge_iff_le, bot_le, sup_of_le_right]
---     congr
---     funext k
---     cases k with
---     | zero => simp [he, Nat.liftBot]
---     | succ k => rfl
---   | reduce p => exact p.effect_le
---   | rw p => rw [p.effect]
---   | rw_op p => rw [p.effect]
diff --git a/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Subst.lean b/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Subst.lean
deleted file mode 100644
index ea01515..0000000
--- a/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Subst.lean
+++ /dev/null
@@ -1,37 +0,0 @@
--- import DeBruijnSSA.BinSyntax.Syntax.Rewrite.Definitions
--- import DeBruijnSSA.BinSyntax.Syntax.Rewrite.Cong
--- import DeBruijnSSA.BinSyntax.Syntax.Rewrite.Directed
-
--- namespace BinSyntax
-
--- variable {φ : Type u} {ε : Type v} [Φ: EffectSet φ ε] [SemilatticeSup ε] [OrderBot ε]
-
--- namespace Region
-
--- inductive CongD.SubstCong (P : Region φ → Region φ → Type _) : Subst φ → Subst φ → Type _
---   | step (n) : CongD P r r' → SubstCong P (Function.update σ n r) (Function.update σ' n r')
-
--- inductive BCongD.SubstCong (P : (ℕ → ε) → Region φ → Region φ → Type _)
---   : (ℕ → ε) → Subst φ → Subst φ → Type _
---   | step (n) : BCongD P Γ r r' → SubstCong P Γ (Function.update σ n r) (Function.update σ' n r')
-
--- def RWD.Subst (P : (ℕ → ε) →  Region φ → Region φ → Type _) (Γ : ℕ → ε) (σ σ' : Subst φ)
---   := ∀n, RWD P Γ (σ n) (σ' n)
-
--- -- TODO: RwD.Subst is effect monotone/antitone iff underlying is
--- -- ==> RwD.Subst is effect preserving iff underlying is
-
--- def RWD.Subst.refl {P} {Γ : ℕ → ε} (σ : Region.Subst φ) : RWD.Subst P Γ σ σ := λ_ => RWD.refl _
-
--- def RWD.Subst.comp {P} {Γ : ℕ → ε} {σ σ' σ'' : Region.Subst φ}
---   (h : RWD.Subst P Γ σ σ') (h' : RWD.Subst P Γ σ' σ'')
---   : RWD.Subst P Γ σ σ''
---   := λn => (h n).comp (h' n)
-
--- -- TODO: lift, liftn, lwk, vwk lore
-
--- -- TODO: Path SubstCong ==> RWD, RWD ∩ FiniteDiff ==> Path SubstCong, "adjunction"
-
--- end Region
-
--- end BinSyntax
diff --git a/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Term/Step.lean b/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Term/Step.lean
index 54d78ef..9cec7e6 100644
--- a/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Term/Step.lean
+++ b/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Term/Step.lean
@@ -23,10 +23,6 @@ inductive Rewrite : Term φ → Term φ → Prop
     Rewrite (let1 (let1 a b) r) (let1 a $ let1 b $ r.wk1)
   | let1_let2 (a b r) :
     Rewrite (let1 (let2 a b) r) (let2 a $ let1 b $ r.wk1.wk1)
-  | let1_inl (e r) :
-    Rewrite (let1 (inl e) r) (let1 e $ let1 (inl (var 0)) $ r.wk1)
-  | let1_inr (e r) :
-    Rewrite (let1 (inr e) r) (let1 e $ let1 (inr (var 0)) $ r.wk1)
   | let1_case (a l r s) :
     Rewrite (let1 (case a l r) s) (case a (let1 l $ s.wk1) (let1 r $ s.wk1))
   | let1_abort (e r) :
@@ -66,12 +62,6 @@ theorem Rewrite.subst {e e' : Term φ} (h : e.Rewrite e') (σ) : (e.subst σ).Re
   | let1_let2 a b r =>
     simp only [Term.subst, <-wk1_subst_lift, Subst.liftn_two]
     exact let1_let2 (a.subst σ) (b.subst σ.lift.lift) (r.subst σ.lift)
-  | let1_inl e r =>
-    simp only [Term.subst, <-wk1_subst_lift]
-    exact let1_inl (e.subst σ) (r.subst (σ.lift))
-  | let1_inr e r =>
-    simp only [Term.subst, <-wk1_subst_lift]
-    exact let1_inr (e.subst σ) (r.subst (σ.lift))
   | let1_case a l r s =>
     simp only [Term.subst, <-wk1_subst_lift]
     exact let1_case (a.subst σ) (l.subst σ.lift) (r.subst σ.lift) (s.subst σ.lift)