diff --git a/DeBruijnSSA/BinSyntax/Syntax/Fv/Subst.lean b/DeBruijnSSA/BinSyntax/Syntax/Fv/Subst.lean
index 6f4fa29..fabe179 100644
--- a/DeBruijnSSA/BinSyntax/Syntax/Fv/Subst.lean
+++ b/DeBruijnSSA/BinSyntax/Syntax/Fv/Subst.lean
@@ -150,11 +150,12 @@ theorem Term.Subst.eqOn_lift_iff {σ σ' : Term.Subst φ} {s : Set ℕ}
   · rw [Set.mem_liftFv] at hn
     have h := h hn
     simp only [lift_succ] at h
-    sorry
-  · sorry
+    exact Term.wk0_injective h
+  · cases n with | zero => rfl | _ => simp [Subst.lift, h ((Set.mem_liftFv _ _).mpr hn)]
 
 theorem Term.Subst.eqOn_liftn_iff {σ σ' : Term.Subst φ} {s : Set ℕ}
-  : s.EqOn (σ.liftn n) (σ'.liftn n) ↔ (s.liftnFv n).EqOn σ σ' := sorry
+  : s.EqOn (σ.liftn n) (σ'.liftn n) ↔ (s.liftnFv n).EqOn σ σ' := by
+  induction n generalizing σ σ' s <;> simp [Subst.liftn_succ', Set.liftnFv_succ', eqOn_lift_iff, *]
 
 theorem Term.subst_eq_iff {t : Term φ} {σ σ' : Subst φ}
   : t.subst σ = t.subst σ' ↔ t.fvs.EqOn σ σ' := by induction t generalizing σ σ' with
@@ -219,8 +220,8 @@ theorem Region.vsubst_eqOn_fvs {r : Region φ} {σ σ' : Term.Subst φ} (h : r.f
 theorem Region.vsubst_eqOn_fvi {r : Region φ} {σ σ' : Term.Subst φ} (h : (Set.Iio r.fvi).EqOn σ σ')
   : r.vsubst σ = r.vsubst σ' := r.vsubst_eqOn_fvs (h.mono r.fvs_fvi)
 
-theorem Region.lsubst_eqOn_fls {r : Region φ} {σ σ' : Subst φ} (h : r.fls.EqOn σ σ')
-  : r.lsubst σ = r.lsubst σ' := by sorry
+-- theorem Region.lsubst_eqOn_fls {r : Region φ} {σ σ' : Subst φ} (h : r.fls.EqOn σ σ')
+--   : r.lsubst σ = r.lsubst σ' := by sorry
 
 -- TODO: {Terminator, Region}.Subst.{fv, fl}
 
diff --git a/DeBruijnSSA/BinSyntax/Syntax/Subst.lean b/DeBruijnSSA/BinSyntax/Syntax/Subst.lean
index d6cdfe3..a4fbfaa 100644
--- a/DeBruijnSSA/BinSyntax/Syntax/Subst.lean
+++ b/DeBruijnSSA/BinSyntax/Syntax/Subst.lean
@@ -1,1847 +1,3 @@
-import Discretion.Wk.Nat
-import Discretion.Wk.Fin
-import Discretion.Wk.Multiset
-import Discretion.Wk.Multiset
-
-import DeBruijnSSA.BinSyntax.Syntax.Definitions
-
-namespace BinSyntax
-
-/-! ### Term substitutions
- -/
-namespace Term
-
-/-- A substitution mapping variables to terms -/
-def Subst (φ : Type _) := ℕ → Term φ -- TODO: Term.Subst?
-
-/-- The identity substitution, which simply maps variables to themselves -/
-def Subst.id : Subst φ := Term.var
-
-@[simp]
-theorem Subst.id_apply (n : ℕ) : @Subst.id φ n = Term.var n := rfl
-
-/-- Lift a substitution under a binder -/
-def Subst.lift (σ : Subst φ) : Subst φ
-  | 0 => Term.var 0
-  | n + 1 => (σ n).wk Nat.succ
-
-@[simp]
-theorem Subst.lift_zero (σ : Subst φ) : σ.lift 0 = Term.var 0 := rfl
-
-@[simp]
-theorem Subst.lift_succ (σ : Subst φ) (i : ℕ) : σ.lift (i + 1) = (σ i).wk Nat.succ := rfl
-
-/-- Lift a substitution under `n` binders -/
-def Subst.liftn (n : ℕ) (σ : Subst φ) : Subst φ
-  := λm => if m < n then Term.var m else (σ (m - n)).wk (λv => v + n)
-
-@[simp]
-theorem Subst.liftn_zero (σ : Subst φ) : σ.liftn 0 = σ := by
-  funext n
-  simp only [liftn]
-  split
-  · rename_i H; cases H
-  · exact (σ n).wk_id
-
-theorem Subst.liftn_one (σ : Subst φ) : σ.liftn 1 = σ.lift := by funext m; cases m <;> rfl
-
-theorem Subst.liftn_succ (n) (σ: Subst φ) : σ.liftn n.succ = (σ.liftn n).lift := by
-  induction n with
-  | zero => rw [σ.liftn_one, σ.liftn_zero]
-  | succ n I => -- TODO: I'm sure this can be made _much_ cleaner...
-    funext m
-    rw [I]
-    simp only [lift]
-    split
-    · rfl
-    · simp only [liftn]
-      split
-      · split
-        · rfl
-        · split
-          · rfl
-          · rename_i H C; exact (C (Nat.lt_of_succ_lt_succ (Nat.lt_of_succ_lt_succ H))).elim
-      · split
-        · rename_i H; simp_arith at H
-        · split
-          · rename_i C H; exact (C (Nat.succ_lt_succ (Nat.succ_lt_succ H))).elim
-          · simp only [Term.wk_wk]
-            apply congr
-            apply congrArg
-            funext v
-            simp_arith
-            simp_arith
-
-theorem Subst.liftn_two (σ: Subst φ) : σ.liftn 2 = σ.lift.lift
-  := by rw [Subst.liftn_succ, Subst.liftn_one]
-
-theorem Subst.liftn_eq_iterate_lift_apply (n: ℕ) (σ: Subst φ) : σ.liftn n = (Subst.lift^[n] σ) := by
-  induction n with
-  | zero => exact σ.liftn_zero
-  | succ n I => simp only [Function.iterate_succ_apply', Subst.liftn_succ, *]
-
-theorem Subst.liftn_eq_iterate_lift (n: ℕ) : Subst.liftn n = (@Subst.lift φ)^[n] := by
-  funext σ
-  rw [liftn_eq_iterate_lift_apply]
-
-theorem Subst.liftn_succ' (n) (σ: Subst φ) : σ.liftn n.succ = σ.lift.liftn n := by
-  simp [liftn_eq_iterate_lift]
-
-@[simp]
-theorem Subst.lift_id : (@id φ).lift = id := by funext n; cases n <;> rfl
-
-@[simp]
-theorem Subst.iterate_lift_id : (n: ℕ) -> Subst.lift^[n] (@id φ) = id
-  | 0 => rfl
-  | n + 1 => by simp [lift_id, iterate_lift_id n]
-
-@[simp]
-theorem Subst.liftn_id (n: ℕ): (@id φ).liftn n = id := by
-  rw [liftn_eq_iterate_lift_apply, iterate_lift_id]
-
-theorem Subst.liftn_add (n m: ℕ) : Subst.liftn (m + n) = (@Subst.liftn α m) ∘ (@Subst.liftn α n)
-  := by simp [liftn_eq_iterate_lift, Function.iterate_add]
-
-theorem Subst.liftn_liftn (n m: ℕ) (σ: Subst φ): (σ.liftn n).liftn m = σ.liftn (m + n)
-  := by simp [liftn_add]
-
-theorem Subst.liftn_liftn' (n m: ℕ) (σ: Subst φ): (σ.liftn n).liftn m = σ.liftn (n + m)
-  := by simp [liftn_liftn, Nat.add_comm]
-
-/-- Substitute the free variables in a `Term` using `σ` -/
-@[simp]
-def subst (σ : Subst φ) : Term φ → Term φ
-| var x => σ x
-| op f x => op f (subst σ x)
-| let1 a e => let1 (subst σ a) (subst σ.lift e)
-| pair x y => pair (subst σ x) (subst σ y)
-| unit => unit
-| let2 a e => let2 (subst σ a) (subst (σ.liftn 2) e)
-| inl a => inl (subst σ a)
-| inr a => inr (subst σ a)
-| case a l r => case (subst σ a) (subst σ.lift l) (subst σ.lift r)
-| abort a => abort (subst σ a)
-
-@[simp]
-theorem subst_id (t : Term φ) : t.subst Subst.id = t := by induction t <;> simp [*]
-
-theorem Subst.ext_subst (σ τ : Subst φ) (h : ∀t : Term φ, t.subst σ = t.subst τ) : ∀n, σ n = τ n
-  := λn => h (var n)
-
--- i.e. subst is a faithful functor
-theorem subst_injective : Function.Injective (@subst φ)
-  := λσ τ h => funext (λn => σ.ext_subst τ (λ_ => h ▸ rfl) n)
-
-/-- Create a substitution from a variable renaming -/
-def Subst.fromWk (ρ : ℕ -> ℕ): Subst φ := Term.var ∘ ρ
-
-@[simp]
-theorem Subst.fromWk_apply (ρ : ℕ -> ℕ) (n : ℕ) : (@fromWk φ ρ) n = Term.var (ρ n) := rfl
-
-theorem Subst.fromWk_lift (ρ) : (@fromWk φ ρ).lift = fromWk (Nat.liftWk ρ) := by
-  funext n; cases n <;> rfl
-
-theorem Subst.fromWk_iterate_lift
-  : (n : ℕ) -> ∀ρ, Subst.lift^[n] (@fromWk φ ρ) = fromWk (Nat.liftWk^[n] ρ)
-  | 0, ρ => rfl
-  | n + 1, ρ => by simp [fromWk_lift, fromWk_iterate_lift n]
-
-theorem Subst.fromWk_liftn (n ρ) : (@fromWk φ ρ).liftn n = fromWk (Nat.liftnWk n ρ) := by
-  rw [liftn_eq_iterate_lift, Nat.liftnWk_eq_iterate_liftWk, fromWk_iterate_lift]
-
-theorem subst_fromWk_apply (ρ : ℕ -> ℕ) (t : Term φ) : t.subst (Subst.fromWk ρ) = t.wk ρ := by
-  induction t generalizing ρ <;> simp [Subst.fromWk_liftn, Term.Subst.fromWk_lift,  *]
-
-theorem subst_fromWk (ρ : ℕ -> ℕ) : @Term.subst φ (Subst.fromWk ρ) = Term.wk ρ
-  := funext (subst_fromWk_apply ρ)
-
-theorem subst_comp_fromWk : @Term.subst φ ∘ Subst.fromWk = Term.wk
-  := funext subst_fromWk
-
-theorem subst_liftn (n : ℕ) (σ : Subst φ) (t : Term φ)
-    : (t.wk (Nat.liftnWk n Nat.succ)).subst (σ.liftn (n + 1))
-      = (t.subst (σ.liftn n)).wk (Nat.liftnWk n Nat.succ)
-  := by induction t generalizing σ n with
-  | var =>
-    --TODO: how should this be factored?
-    simp only [wk, subst, Nat.liftnWk, Subst.liftn]
-    split
-    · split
-      · simp [Nat.liftnWk, *]
-      · rename_i H C; exact (C (Nat.le_step H)).elim
-    · rename_i C
-      simp_arith only [ite_false, wk_wk]
-      apply congr
-      · apply congrArg
-        funext v
-        simp_arith [Function.comp_apply, Zero.zero, Nat.liftnWk]
-      · simp [Nat.succ_add, Nat.succ_sub_succ, Nat.add_sub_assoc]
-  | _ => simp [
-    <-Subst.liftn_succ, <-Nat.liftnWk_succ_apply', <-Nat.liftnWk_add_apply', Subst.liftn_liftn', *]
-
-theorem subst_iterate_lift (n : ℕ) (σ : Subst φ) (t : Term φ)
-  : (t.wk (Nat.liftWk^[n] Nat.succ)).subst (Subst.lift^[n + 1] σ)
-    = (t.subst (Subst.lift^[n] σ)).wk (Nat.liftWk^[n] Nat.succ)
-  := by simp only [<-Subst.liftn_eq_iterate_lift, <-Nat.liftnWk_eq_iterate_liftWk, subst_liftn]
-
-theorem subst_lift (t : Term φ) (σ : Subst φ)
-  : (t.wk Nat.succ).subst (σ.lift) = (t.subst σ).wk Nat.succ := t.subst_iterate_lift 0 σ
-
-/-- Compose two substitutions on terms to yield another -/
-def Subst.comp (σ τ : Subst φ): Subst φ
-  | n => (τ n).subst σ
-
-theorem Subst.lift_comp (σ τ : Subst φ) : (σ.comp τ).lift = σ.lift.comp τ.lift := by
-  funext n
-  cases n with
-  | zero => rfl
-  | succ n => simp [lift, comp, Term.subst_lift]
-
-theorem Subst.iterate_lift_comp
-  : (n : ℕ) -> ∀σ τ : Subst φ, Subst.lift^[n] (σ.comp τ)
-    = (Subst.lift^[n] σ).comp (Subst.lift^[n] τ)
-  | 0, σ, τ => rfl
-  | n + 1, σ, τ => by simp [Subst.lift_comp, iterate_lift_comp n]
-
-theorem Subst.liftn_comp (n : ℕ) (σ τ : Subst φ)
-  : (σ.comp τ).liftn n = (σ.liftn n).comp (τ.liftn n)
-  := by rw [liftn_eq_iterate_lift, iterate_lift_comp]
-
-theorem subst_comp (σ τ : Subst φ) (t : Term φ) : t.subst (σ.comp τ) = (t.subst τ).subst σ
-  := by induction t generalizing σ τ with
-  | var => rfl
-  | _ => simp [subst, Subst.lift_comp, Subst.liftn_comp, *]
-
-theorem subst_subst (σ τ : Subst φ) (t : Term φ)
-  : (t.subst τ).subst σ = t.subst (σ.comp τ) := by rw [subst_comp]
-
-@[simp]
-theorem Subst.comp_id (σ : Subst φ) : σ.comp Subst.id = σ := by funext n; rfl
-
-@[simp]
-theorem Subst.id_comp (σ : Subst φ) : Subst.id.comp σ = σ := by funext n; simp [comp]
-
-theorem Subst.comp_assoc (σ τ ρ : Subst φ) : (σ.comp τ).comp ρ = σ.comp (τ.comp ρ) := by
-  funext n
-  simp only [comp, Function.comp_apply, subst_comp]
-
-/-- Substitute a term for the smallest variable, bumping the rest downwards -/
-def subst0 (t : Term φ) : Subst φ
-  | 0 => t
-  | n + 1 => var n
-
-@[simp]
-theorem subst0_zero (t : Term φ) : subst0 t 0 = t := rfl
-
-@[simp]
-theorem subst0_succ (t : Term φ) (n : ℕ) : subst0 t (n + 1) = var n := rfl
-
-theorem subst_subst0_wk (e s : Term φ) (ρ)
-  : (e.subst s.subst0).wk ρ = (e.wk (Nat.liftWk ρ)).subst (s.wk ρ).subst0 := by
-  simp only [<-subst_fromWk_apply, subst_subst]
-  congr
-  funext n
-  cases n <;> rfl
-
-theorem subst0_comp_wk (s : Term φ)
-  : (Subst.fromWk ρ).comp (subst0 s) = (s.wk ρ).subst0.comp (Subst.fromWk (Nat.liftWk ρ))
-  := by funext n; cases n <;> simp [Subst.comp, subst_fromWk_apply]
-
-theorem subst0_var0 : @subst0 φ (var 0) = Subst.fromWk Nat.pred := by funext n; cases n <;> rfl
-
-@[simp]
-theorem wk_succ_comp_subst0 (e : Term φ) : e.subst0.comp (Subst.fromWk Nat.succ) = Subst.id
-  := by funext n; cases n <;> rfl
-
-@[simp]
-theorem wk_succ_subst_subst0 (e s : Term φ) : (e.wk Nat.succ).subst s.subst0 = e := by
-  rw [<-subst_fromWk_apply, <-subst_comp, wk_succ_comp_subst0, subst_id]
-
-@[simp]
-theorem subst0_wk0 (e s : Term φ) : e.wk0.subst s.subst0 = e := wk_succ_subst_subst0 e s
-
-@[simp]
-theorem wk1_subst0_var0 (e : Term φ) : e.wk1.subst (var 0).subst0 = e := by
-  rw [subst0_var0, subst_fromWk, wk1, wk_wk]
-  apply Eq.trans _ e.wk_id
-  congr
-  funext i
-  cases i <;> rfl
-
-@[simp]
-theorem wk1_subst0_var0' (e : Term φ) : (e.wk (Nat.liftWk Nat.succ)).subst (var 0).subst0 = e
-  := e.wk1_subst0_var0
-
-/-- Substitute a term for the `n`th variable, bumping those above it downwards -/
-def substn (n : ℕ) (t : Term φ) : Subst φ := λm =>
-  if m < n then var m else if m = n then t else var (m - 1)
-
-theorem substn_zero (t : Term φ) : substn 0 t = subst0 t := by
-  funext n; cases n <;> rfl
-
-theorem substn_succ (n : ℕ) (t : Term φ)
-  : substn (n + 1) (t.wk Nat.succ) = (substn n t).lift := by
-  funext m
-  cases m with
-  | zero => simp [substn]
-  | succ m =>
-    simp only [substn, Nat.add_lt_add_iff_right, add_left_inj, Nat.add_sub_cancel, Subst.lift]
-    split
-    case isTrue => rfl
-    case isFalse h =>
-      split
-      case isTrue => rfl
-      case isFalse h' =>
-        simp only [wk, Nat.succ_eq_add_one, var.injEq]
-        rw [Nat.sub_add_cancel]
-        exact Nat.succ_le_of_lt $ Nat.lt_of_le_of_lt
-          (Nat.zero_le n)
-          (Nat.lt_of_le_of_ne (Nat.le_of_not_lt h) (Ne.symm h'))
-
-theorem substn_add (n m : ℕ) (t : Term φ)
-  : substn (n + m) (t.wk (· + m)) = (substn n t).liftn m := by
-  induction m with
-  | zero => simp
-  | succ m I => rw [Subst.liftn_succ, <-I, <-substn_succ, <-Nat.add_assoc, wk_wk]; rfl
-
-theorem substn_add_right (n m : ℕ) (t : Term φ)
-  : substn (m + n) (t.wk (· + m)) = (substn n t).liftn m := Nat.add_comm _ _ ▸ substn_add n m t
-
-@[simp]
-theorem substn_n (n : ℕ) (t : Term φ) : substn n t n = t := by simp [substn]
-
-theorem subst_substn_wk (e s : Term φ) (ρ) (n)
-  : (e.subst (s.substn n)).wk (Nat.liftnWk n ρ)
-  = (e.wk (Nat.liftnWk (n + 1) ρ)).subst ((s.wk (Nat.liftnWk n ρ)).substn n) := by
-  simp only [<-subst_fromWk_apply, subst_subst]
-  congr
-  funext k
-  simp only [Subst.fromWk, Subst.comp, wk, substn, subst, Nat.liftnWk]
-  split
-  case isTrue h =>
-    have h' : k < n + 1 := Nat.lt_succ_of_lt h
-    simp only [wk, h, h', Nat.liftnWk, ↓reduceIte]
-    simp only [subst, Function.comp_apply, Nat.liftnWk, var.injEq, ite_eq_left_iff, not_lt]
-    exact λhk => (Nat.not_le_of_lt h hk).elim
-  case isFalse h =>
-    split
-    case isTrue h =>
-      cases h
-      simp
-    case isFalse h' =>
-      have hn : ¬k ≤ n := match Nat.eq_or_lt_of_not_lt h with
-        | Or.inl h => (h' h).elim
-        | Or.inr h => Nat.not_le_of_lt h
-      have h' : ¬k < n + 1 := match Nat.eq_or_lt_of_not_lt h with
-        | Or.inl h => (h' h).elim
-        | Or.inr h => Nat.not_lt_of_le h
-      have h'' : ¬k - 1 < n := λc => (hn (Nat.le_of_pred_lt c)).elim
-      have hρ : ρ (k - 1 - n) = ρ (k - (n + 1)) := by simp [Nat.add_comm n 1, Nat.sub_add_eq]
-      simp_arith [h', h'', Nat.liftnWk, hρ]
-
-theorem liftn_subst0 (n : ℕ) (t : Term φ) : t.subst0.liftn n = (t.wk (· + n)).substn n := by
-  induction n with
-  | zero => simp [substn_zero]
-  | succ n I =>
-    rw [Subst.liftn_succ, I]
-    have h : (· + (n + 1)) = Nat.succ ∘ (· + n) := by funext m; simp_arith
-    rw [h, <-Term.wk_wk, substn_succ]
-
-theorem subst_liftn_subst0_wk (e s : Term φ) (ρ n)
-  : (e.subst (s.subst0.liftn n)).wk (Nat.liftnWk n ρ)
-  = (e.wk (Nat.liftnWk (n + 1) ρ)).subst ((s.wk ρ).subst0.liftn n)
-  := by
-  simp only [liftn_subst0, subst_substn_wk, wk_wk]
-  congr
-  apply congrArg
-  congr
-  funext k
-  simp [Nat.liftnWk]
-
-/-- Substitute a term for the `n`th variable, leaving the rest unchanged -/
-def alpha (n : ℕ) (t : Term φ) : Subst φ := Function.update Subst.id n t
-
-@[simp]
-theorem wk1_comp_subst0 (e : Term φ)
-  : e.subst0.comp (Subst.fromWk (Nat.wkn 1)) = e.alpha 0
-  := by funext n; cases n <;> rfl
-
-@[simp]
-theorem liftWk_succ_comp_subst0 (e : Term φ)
-  : e.subst0.comp (Subst.fromWk (Nat.liftWk Nat.succ)) = e.alpha 0
-  := by funext n; cases n <;> rfl
-
-@[simp]
-theorem wkn_comp_substn_succ (n : ℕ) (e : Term φ)
-  : (e.substn n).comp (Subst.fromWk (Nat.wkn (n + 1))) = e.alpha n := by
-  funext i
-  simp only [Subst.comp, subst, substn, Nat.wkn, alpha, Function.update, eq_rec_constant,
-    Subst.id_apply, dite_eq_ite, Nat.lt_succ_iff]
-  split
-  case isTrue h =>
-    split
-    case isTrue h' => simp [Nat.ne_of_lt h']
-    case isFalse h' => simp [Nat.le_antisymm h (Nat.le_of_not_lt h')]
-  case isFalse h =>
-    have c : ¬(i + 1 < n) := λc => h (Nat.le_of_lt (Nat.lt_trans (by simp) c))
-    have c' : i + 1 ≠ n := λc => by cases c; simp at h
-    have c'' : i ≠ n := λc => h (Nat.le_of_eq c)
-    simp [c, c', c'']
-
-@[simp]
-theorem alpha_var : (var n).alpha n = @Subst.id φ := by funext n; simp [alpha, Subst.id]
-
-theorem wk0_subst {σ : Subst φ} {e : Term φ}
-  : (e.subst σ).wk0 = e.wk0.subst σ.lift := (subst_lift e σ).symm
-
-theorem wk1_subst_lift {σ : Subst φ} {e : Term φ}
-  : (e.subst σ.lift).wk1 = e.wk1.subst σ.lift.lift := by
-  simp only [wk1, <-subst_fromWk, subst_subst]
-  congr
-  funext k
-  cases k with
-  | zero => rfl
-  | succ k =>
-    simp only [
-      Subst.comp, BinSyntax.Term.subst, Nat.liftWk_succ, Nat.succ_eq_add_one, Subst.lift_succ,
-      wk_wk, subst_fromWk, Nat.liftWk_succ_comp_succ
-    ]
-    rfl
-
-theorem wk2_subst_lift_lift {σ : Subst φ} {e : Term φ}
-  : (e.subst σ.lift.lift).wk2 = e.wk2.subst σ.lift.lift.lift := by
-  simp only [wk2, <-subst_fromWk, subst_subst]
-  congr
-  funext k
-  cases k with
-  | zero => rfl
-  | succ k =>
-    cases k with
-    | zero => rfl
-    | succ k =>
-      simp_arith only [
-        Subst.comp, BinSyntax.Term.subst, Nat.liftWk_succ, Nat.succ_eq_add_one, Subst.lift_succ,
-        wk_wk, subst_fromWk, Nat.liftWk_succ_comp_succ, Nat.liftnWk, ↓reduceIte
-      ]
-      rfl
-
-theorem swap01_subst_lift_lift {σ : Subst φ} {e : Term φ}
-  : (e.subst σ.lift.lift).swap01 = e.swap01.subst σ.lift.lift := by
-  simp only [swap01, <-subst_fromWk, subst_subst]
-  congr
-  funext k
-  cases k with
-  | zero => rfl
-  | succ k =>
-    cases k with
-    | zero => rfl
-    | succ k =>
-      simp_arith only [
-        Subst.comp, BinSyntax.Term.subst, Nat.liftWk_succ, Nat.succ_eq_add_one, Subst.lift_succ,
-        wk_wk, subst_fromWk, Nat.liftWk_succ_comp_succ, Nat.liftnWk, ↓reduceIte, Nat.swap0
-      ]
-      rfl
-
-theorem swap02_subst_lift_lift_lift {σ : Subst φ} {e : Term φ}
-  : (e.subst σ.lift.lift.lift).swap02 = e.swap02.subst σ.lift.lift.lift := by
-  simp only [swap02, <-subst_fromWk, subst_subst]
-  congr
-  funext k
-  cases k with
-  | zero => rfl
-  | succ k =>
-    cases k with
-    | zero => rfl
-    | succ k =>
-      cases k with
-      | zero => rfl
-      | succ k =>
-        simp_arith only [
-          Subst.comp, BinSyntax.Term.subst, Nat.liftWk_succ, Nat.succ_eq_add_one, Subst.lift_succ,
-          wk_wk, subst_fromWk, Nat.liftWk_succ_comp_succ, Nat.liftnWk, ↓reduceIte, Nat.swap0
-        ]
-        rfl
-
-end Term
-
-/-- Substitute the free variables in a body -/
-@[simp]
-def Body.subst (σ : Term.Subst φ) : Body φ → Body φ
-  | nil => nil
-  | let1 e t => let1 (e.subst σ) (t.subst σ.lift)
-  | let2 e t => let2 (e.subst σ) (t.subst (σ.liftn 2))
-
-@[simp]
-theorem Body.subst_id (b : Body φ) : b.subst Term.Subst.id = b := by
-  induction b <;> simp [Term.Subst.lift_id, Term.Subst.liftn_id, *]
-
-theorem Body.subst_comp (σ τ : Term.Subst φ) (b : Body φ)
-  : b.subst (σ.comp τ) = (b.subst τ).subst σ := by
-  induction b generalizing σ τ
-  <;> simp [Term.subst_comp, Term.Subst.lift_comp, Term.Subst.liftn_comp, *]
-
-@[simp]
-theorem Body.num_defs_subst (σ : Term.Subst φ) (b : Body φ)
-  : (b.subst σ).num_defs = b.num_defs := by
-  induction b generalizing σ <;> simp [*]
-
-/-- Substitute the free variables in a `Terminator` using `σ` -/
-@[simp]
-def Terminator.vsubst (σ : Term.Subst φ) : Terminator φ → Terminator φ
-  | br ℓ e => br ℓ (e.subst σ)
-  | case e s t => case (e.subst σ) (vsubst σ.lift s) (vsubst σ.lift t)
-
-@[simp]
-theorem Terminator.vsubst_id (r : Terminator φ) : r.vsubst Term.Subst.id = r := by
-  induction r <;> simp [*]
-
-theorem Terminator.vsubst_vsubst (σ τ : Term.Subst φ) (r : Terminator φ)
-  : (r.vsubst τ).vsubst σ = r.vsubst (σ.comp τ) := by
-  induction r generalizing σ τ
-  <;> simp [Term.subst_comp, Term.Subst.lift_comp, Term.Subst.liftn_comp, *]
-
-theorem Terminator.ext_vsubst (σ τ : Term.Subst φ)
-  (h : ∀t : Terminator φ, t.vsubst σ = t.vsubst τ) : ∀n, σ n = τ n
-  := λn => by
-    have h' := h (br 0 (Term.var n))
-    simp at h'
-    exact h'
-
--- i.e. vsubst is a faithful functor
-theorem Terminator.vsubst_injective : Function.Injective (@Terminator.vsubst φ)
-  := λσ τ h => funext (λn => Terminator.ext_vsubst σ τ (λ_ => h ▸ rfl) n)
-
-theorem Terminator.vsubst_fromWk_apply (ρ : ℕ -> ℕ) (r : Terminator φ)
-  : r.vsubst (Term.Subst.fromWk ρ) = r.vwk ρ := by
-  induction r generalizing ρ
-  <;> simp [Term.subst_fromWk_apply, Term.Subst.fromWk_liftn, Term.Subst.fromWk_lift, *]
-
-theorem Terminator.vsubst_fromWk (ρ : ℕ -> ℕ)
-  : vsubst (Term.Subst.fromWk ρ) = @vwk φ ρ := funext (vsubst_fromWk_apply ρ)
-
-theorem Terminator.vsubst_comp_fromWk
-  : @vsubst φ ∘ Term.Subst.fromWk = @vwk φ := funext vsubst_fromWk
-
-theorem Terminator.lwk_vsubst (σ : Term.Subst φ) (ρ : ℕ -> ℕ) (r : Terminator φ)
-  : (r.vsubst σ).lwk ρ = (r.lwk ρ).vsubst σ := by induction r generalizing σ <;> simp [*]
-
-theorem Terminator.vsubst_lwk (σ : Term.Subst φ) (ρ : ℕ -> ℕ) (r : Terminator φ)
-  : (r.lwk ρ).vsubst σ = (r.vsubst σ).lwk ρ := Eq.symm $ Terminator.lwk_vsubst σ ρ r
-
-@[simp]
-theorem Terminator.vwk_succ_vsubst_subst0 (t : Terminator φ) (s : Term φ)
-  : (t.vwk Nat.succ).vsubst s.subst0 = t := by
-  rw [<-vsubst_fromWk_apply, vsubst_vsubst, Term.wk_succ_comp_subst0, vsubst_id]
-
-/-- Substitute the free variables in a basic block -/
-@[simp]
-def Block.vsubst (σ : Term.Subst φ) (β : Block φ) : Block φ where
-  body := β.body.subst σ
-  terminator := β.terminator.vsubst (σ.liftn β.body.num_defs)
-
-@[simp]
-theorem Block.vsubst_id (β : Block φ) : β.vsubst Term.Subst.id = β := by simp
-
-theorem Block.vsubst_vsubst (σ τ : Term.Subst φ) (β : Block φ)
-  : (β.vsubst τ).vsubst σ = β.vsubst (σ.comp τ)
-  := by simp [
-    Body.subst_comp, Body.num_defs_subst, Term.Subst.liftn_comp, Terminator.vsubst_vsubst, *]
-
-/-- Substitute the free variables in a region -/
-@[simp]
-def BBRegion.vsubst (σ : Term.Subst φ) : BBRegion φ → BBRegion φ
-  | cfg β n f => cfg (β.vsubst σ) n (λ i => (f i).vsubst (σ.liftn (β.body.num_defs + 1)))
-
-@[simp]
-theorem BBRegion.vsubst_id (r : BBRegion φ) : r.vsubst Term.Subst.id = r := by
-  induction r; simp [*]
-
-theorem BBRegion.vsubst_vsubst (σ τ : Term.Subst φ) (r : BBRegion φ)
-  : (r.vsubst τ).vsubst σ = r.vsubst (σ.comp τ) := by
-  induction r generalizing σ τ
-  simp [Body.subst_comp, Body.num_defs_subst, Term.Subst.liftn_comp, Terminator.vsubst_vsubst, *]
-
-/-- Substitute the free variables in a control-flow graph -/
-@[simp]
-def BBCFG.vsubst (σ : Term.Subst φ) (cfg : BBCFG φ) : BBCFG φ where
-  length := cfg.length
-  targets := λi => (cfg.targets i).vsubst σ
-
-@[simp]
-theorem BBCFG.vsubst_id (cfg : BBCFG φ) : cfg.vsubst Term.Subst.id = cfg := by
-  cases cfg; simp [*]
-
-theorem BBCFG.vsubst_vsubst (σ τ : Term.Subst φ) (cfg : BBCFG φ)
-  : (cfg.vsubst τ).vsubst σ = cfg.vsubst (σ.comp τ) := by
-  cases cfg; simp [BBRegion.vsubst_vsubst, *]
-
-/-- Substitute the free variables in a region -/
-@[simp]
-def TRegion.vsubst (σ : Term.Subst φ) : TRegion φ → TRegion φ
-  | let1 e t => let1 (e.subst σ) (t.vsubst σ.lift)
-  | let2 e t => let2 (e.subst σ) (t.vsubst (σ.liftn 2))
-  | cfg β n f => cfg (β.vsubst σ) n (λ i => (f i).vsubst σ.lift)
-
-@[simp]
-theorem TRegion.vsubst_id (r : TRegion φ) : r.vsubst Term.Subst.id = r := by
-  induction r <;> simp [TRegion.vsubst, Term.Subst.lift_id, Term.Subst.liftn_id, *]
-
-theorem TRegion.vsubst_vsubst (σ τ : Term.Subst φ) (r : TRegion φ)
-  : (r.vsubst τ).vsubst σ = r.vsubst (σ.comp τ) := by
-  induction r generalizing σ τ
-  <;> simp [Term.subst_comp, Terminator.vsubst_vsubst, Term.Subst.lift_comp, Term.Subst.liftn_comp, *]
-
-def TCFG.vsubst (σ : Term.Subst φ) (cfg : TCFG φ) : TCFG φ where
-  length := cfg.length
-  targets := λi => (cfg.targets i).vsubst σ
-
-@[simp]
-theorem TCFG.vsubst_id (cfg : TCFG φ) : cfg.vsubst Term.Subst.id = cfg := by
-  cases cfg; simp [TCFG.vsubst, *]
-
-theorem TCFG.vsubst_vsubst (σ τ : Term.Subst φ) (cfg : TCFG φ)
-  : (cfg.vsubst τ).vsubst σ = cfg.vsubst (σ.comp τ) := by
-  cases cfg; simp [TCFG.vsubst, TRegion.vsubst_vsubst, *]
-
-/-- Substitute the free variables in a `Region` using `σ` -/
-@[simp]
-def Region.vsubst (σ : Term.Subst φ) : Region φ → Region φ
-  | br n e => br n (e.subst σ)
-  | case e s t => case (e.subst σ) (vsubst σ.lift s) (vsubst σ.lift t)
-  | let1 e t => let1 (e.subst σ) (vsubst σ.lift t)
-  | let2 e t => let2 (e.subst σ) (vsubst (σ.liftn 2) t)
-  | cfg β n f => cfg (vsubst σ β) n (λ i => (f i).vsubst σ.lift)
-
-@[simp]
-theorem Region.vsubst_id (r : Region φ) : r.vsubst Term.Subst.id = r := by
-  induction r <;> simp [*]
-
-theorem Region.vsubst_id' (r : Region φ) (h : σ = Term.Subst.id) : r.vsubst σ = r := by
-  cases h; simp
-
-theorem Region.vsubst_comp_apply (σ τ : Term.Subst φ) (r : Region φ)
-  : r.vsubst (σ.comp τ) = (r.vsubst τ).vsubst σ := by
-  induction r generalizing σ τ
-  <;> simp [Term.subst_comp, Term.Subst.lift_comp, Term.Subst.liftn_comp, *]
-
-theorem Region.vsubst_vsubst (σ τ : Term.Subst φ) (r : Region φ)
-  : (r.vsubst τ).vsubst σ = r.vsubst (σ.comp τ) := by
-  induction r generalizing σ τ
-  <;> simp [Term.subst_comp, Term.Subst.lift_comp, Term.Subst.liftn_comp, *]
-
-theorem Region.vsubst_comp (σ τ : Term.Subst φ)
-  : vsubst σ ∘ vsubst τ = vsubst (σ.comp τ) := by
-  funext r; simp [vsubst_vsubst]
-
-theorem Region.ext_vsubst (σ τ : Term.Subst φ)
-  (h : ∀t : Region φ, t.vsubst σ = t.vsubst τ) : ∀n, σ n = τ n
-  := λn => by
-    have h' := h (br 0 (Term.var n))
-    simp at h'
-    exact h'
-
-theorem Region.vsubst_cfg (σ : Term.Subst φ) (β : Region φ) (n : ℕ) (G : Fin n -> Region φ)
-  : (cfg β n G).vsubst σ = cfg (β.vsubst σ) n (λi => (G i).vsubst σ.lift) := rfl
-
-theorem Region.vsubst_cfg1 (σ : Term.Subst φ) (β : Region φ) (G : Region φ)
-  : (cfg β 1 (Fin.elim1 G)).vsubst σ = cfg (β.vsubst σ) 1 (Fin.elim1 (G.vsubst σ.lift)) := by
-  simp only [vsubst, cfg.injEq, heq_eq_eq, true_and]
-  funext i; cases i using Fin.elim1; rfl
-
--- i.e. vsubst is a faithful functor
-theorem Region.vsubst_injective : Function.Injective (@Region.vsubst φ)
-  := λσ τ h => funext (λn => Region.ext_vsubst σ τ (λ_ => h ▸ rfl) n)
-
-theorem Region.vsubst_fromWk_apply (ρ : ℕ -> ℕ) (r : Region φ)
-  : r.vsubst (Term.Subst.fromWk ρ) = r.vwk ρ := by
-  induction r generalizing ρ
-  <;> simp [Term.subst_fromWk_apply, Term.Subst.fromWk_liftn, Term.Subst.fromWk_lift, *]
-
-theorem Region.vsubst_fromWk (ρ : ℕ -> ℕ)
-  : vsubst (Term.Subst.fromWk ρ) = @vwk φ ρ := funext (vsubst_fromWk_apply ρ)
-
-theorem Region.vsubst0_var0_vwk1 (r : Region φ)
-  : r.vwk1.vsubst (Term.subst0 (Term.var 0)) = r := by
-  rw [vwk1, <-vsubst_fromWk, vsubst_vsubst, vsubst_id']
-  funext k; cases k <;> rfl
-
-theorem Region.vsubst_comp_fromWk
-  : @vsubst φ ∘ Term.Subst.fromWk = @vwk φ := funext vsubst_fromWk
-
-theorem Region.vsubst0_var0_comp_vwk1
-  : vsubst (Term.subst0 (Term.var 0)) ∘ vwk1 (φ := φ) = id
-  := funext vsubst0_var0_vwk1
-
-theorem Region.lwk_vsubst (σ : Term.Subst φ) (ρ : ℕ -> ℕ) (r : Region φ)
-  : (r.vsubst σ).lwk ρ = (r.lwk ρ).vsubst σ := by induction r generalizing σ ρ <;> simp [*]
-
-theorem Region.vsubst_lwk (σ : Term.Subst φ) (ρ : ℕ -> ℕ) (r : Region φ)
-  : (r.lwk ρ).vsubst σ = (r.vsubst σ).lwk ρ := Eq.symm $ Region.lwk_vsubst σ ρ r
-
-theorem Region.lwk1_vsubst (σ : Term.Subst φ) (r : Region φ)
-  : (r.vsubst σ).lwk1 = (r.lwk1).vsubst σ := by rw [lwk1, lwk_vsubst]
-
-theorem Region.vsubst_lwk1 (σ : Term.Subst φ) (r : Region φ)
-  : (r.lwk1).vsubst σ = (r.vsubst σ).lwk1 := by rw [lwk1, vsubst_lwk]
-
-/-- Substitute the free variables in a `CFG` using `σ` -/
-def CFG.vsubst (σ : Term.Subst φ) (G : CFG φ) : CFG φ where
-  length := G.length
-  targets := λ i => (G.targets i).vsubst σ
-
-@[simp]
-theorem CFG.vsubst_id (G : CFG φ) : G.vsubst Term.Subst.id = G := by cases G; simp [vsubst]
-
-theorem CFG.vsubst_comp_apply (σ τ : Term.Subst φ) (G : CFG φ) : G.vsubst (σ.comp τ) = (G.vsubst τ).vsubst σ
-  := by cases G; simp only [CFG.vsubst, Region.vsubst_comp_apply, *]
-
-/-! ### Terminator substitutions
- -/
-namespace Terminator
-
-/-- A substitution mapping labels to terminators -/
-def Subst (φ : Type _) := ℕ → Terminator φ
-
-/-- The identity substitution, which maps labels to themselves -/
-def Subst.id : Subst φ := λn => Terminator.br n (Term.var 0)
-
-theorem Subst.id_apply (n : ℕ) : @Subst.id φ n = Terminator.br n (Term.var 0) := rfl
-
-/-- Lift a substitution under a label binder -/
-def Subst.lift (σ : Subst φ) : Subst φ
-  | 0 => Terminator.br 0 (Term.var 0)
-  | n + 1 => (σ n).lwk Nat.succ
-
-/-- Lift a substitution under `n` label binders -/
-def Subst.liftn (n : ℕ) (σ : Subst φ) : Subst φ
-  := λm => if m < n then Terminator.br m (Term.var 0) else (σ (m - n)).lwk (λv => v + n)
-
-@[simp]
-theorem Subst.liftn_zero (σ : Subst φ) : σ.liftn 0 = σ := by
-  funext n
-  simp only [liftn]
-  split
-  · rename_i H; cases H
-  · exact (σ n).lwk_id
-
-theorem Subst.liftn_one (σ : Subst φ) : σ.liftn 1 = σ.lift := by funext m; cases m <;> rfl
-
-theorem Subst.liftn_succ (n) (σ: Subst φ) : σ.liftn n.succ = (σ.liftn n).lift := by
-  induction n with
-  | zero => rw [σ.liftn_one, σ.liftn_zero]
-  | succ n I => -- TODO: I'm sure this can be made _much_ cleaner...
-    funext m
-    rw [I]
-    simp only [lift]
-    split
-    · rfl
-    · simp only [liftn]
-      split
-      · split
-        · rfl
-        · split
-          · rfl
-          · rename_i H C; exact (C (Nat.lt_of_succ_lt_succ (Nat.lt_of_succ_lt_succ H))).elim
-      · split
-        · rename_i H; simp_arith at H
-        · split
-          · rename_i C H; exact (C (Nat.succ_lt_succ (Nat.succ_lt_succ H))).elim
-          · simp only [Terminator.lwk_lwk]
-            apply congr
-            apply congrArg
-            funext v
-            simp_arith
-            simp_arith
-
-theorem Subst.liftn_two (σ : Subst φ) : σ.liftn 2 = σ.lift.lift := by
-  rw [Subst.liftn_succ, Subst.liftn_succ]; simp
-
-theorem Subst.liftn_eq_iterate_lift_apply (n: ℕ) (σ: Subst φ) : σ.liftn n = (Subst.lift^[n] σ)
-  := by induction n with
-  | zero => exact σ.liftn_zero
-  | succ n => simp only [Function.iterate_succ_apply', Subst.liftn_succ, *]
-
-theorem Subst.liftn_eq_iterate_lift (n: ℕ) : Subst.liftn n = (@Subst.lift φ)^[n] := by
-  funext σ
-  rw [liftn_eq_iterate_lift_apply]
-
-theorem Subst.liftn_succ' (n) (σ: Subst φ) : σ.liftn n.succ = σ.lift.liftn n := by
-  simp [liftn_eq_iterate_lift]
-
-@[simp]
-theorem Subst.lift_id : (@id φ).lift = id := by funext n; cases n <;> rfl
-
-@[simp]
-theorem Subst.iterate_lift_id : (n: ℕ) -> Subst.lift^[n] (@id φ) = id
-  | 0 => rfl
-  | n + 1 => by simp [lift_id, iterate_lift_id n]
-
-@[simp]
-theorem Subst.liftn_id (n: ℕ): (@id φ).liftn n = id := by
-  rw [liftn_eq_iterate_lift_apply, iterate_lift_id]
-
-theorem Subst.liftn_add (n m: ℕ) : Subst.liftn (m + n) = (@Subst.liftn α m) ∘ (@Subst.liftn α n)
-  := by simp [liftn_eq_iterate_lift, Function.iterate_add]
-
-theorem Subst.liftn_liftn (n m: ℕ) (σ: Subst φ): (σ.liftn n).liftn m = σ.liftn (m + n)
-  := by simp [liftn_add]
-
-theorem Subst.lift_succ (σ : Subst φ) (i : ℕ) : σ.lift (i + 1) = (σ i).lwk Nat.succ := rfl
-
-/-- Lift a substitution under a variable binder -/
-def Subst.vlift (σ : Subst φ) : Subst φ := vwk1 ∘ σ
-
-@[simp]
-theorem Subst.vlift_id : (@id φ).vlift = id := by funext v; cases v <;> rfl
-
-theorem Subst.vlift_lift_comm (σ : Subst σ) : σ.lift.vlift = σ.vlift.lift := by
-  funext n
-  cases n with
-  | zero => rfl
-  | succ n => simp [Subst.vlift, lift, vwk_lwk, vwk1]
-
-theorem Subst.vlift_lift_comp_comm : Subst.vlift ∘ (@Subst.lift φ) = Subst.lift ∘ Subst.vlift
-  := funext Subst.vlift_lift_comm
-
-theorem Subst.vlift_liftn_comm (n : ℕ) (σ : Subst σ) : (σ.liftn n).vlift = σ.vlift.liftn n := by
-  induction n generalizing σ with
-  | zero => simp
-  | succ _ I => rw [liftn_succ, vlift_lift_comm, I, liftn_succ]
-
-/-- Lift a substitution under `n` variable binders -/
-def Subst.vliftn (n : ℕ) (σ : Subst φ) : Subst φ
-  := Terminator.vwk (Nat.liftWk (λi => i + n)) ∘ σ
-
-@[simp]
-theorem Subst.vliftn_zero (σ : Subst φ) : σ.vliftn 0 = σ := by
-  funext n
-  simp [vliftn]
-
-theorem Subst.vliftn_one (σ : Subst φ) : σ.vliftn 1 = σ.vlift := by
-  funext n
-  simp [vliftn, vlift, vwk1]
-
-theorem Subst.vliftn_succ (σ : Subst φ) (i : ℕ) : σ.vliftn (i + 1) = (σ.vliftn i).vlift := by
-  funext ℓ
-  simp only [vliftn, Function.comp_apply, vlift, vwk_vwk, vwk1]
-  congr
-  funext n
-  cases n <;> rfl
-
-theorem Subst.vliftn_two (σ : Subst φ) : σ.vliftn 2 = σ.vlift.vlift := by
-  rw [Subst.vliftn_succ, Subst.vliftn_succ]; simp
-
-theorem Subst.vliftn_eq_iterate_vlift_apply (n: ℕ) (σ: Subst φ) : σ.vliftn n = (Subst.vlift^[n] σ)
-  := by induction n with
-  | zero => exact σ.vliftn_zero
-  | succ n => simp only [Function.iterate_succ_apply', Subst.vliftn_succ, *]
-
-theorem Subst.vliftn_eq_iterate_vlift (n: ℕ) : Subst.vliftn n = (@Subst.vlift φ)^[n] := by
-  funext σ
-  rw [vliftn_eq_iterate_vlift_apply]
-
-theorem Subst.vliftn_succ' (σ : Subst φ) (i : ℕ) : σ.vliftn (i + 1) = σ.vlift.vliftn i
-  := by simp [vliftn_eq_iterate_vlift]
-
-theorem Subst.vliftn_add (σ : Subst φ) (n m: ℕ) : σ.vliftn (n + m) = (σ.vliftn m).vliftn n := by
-  funext k
-  simp [vliftn_eq_iterate_vlift, Function.iterate_add_apply]
-
-theorem Subst.iterate_vlift_id : (n: ℕ) -> Subst.vlift^[n] (@id φ) = id
-  | 0 => rfl
-  | n + 1 => by simp [Subst.vlift_id, iterate_vlift_id n]
-
-theorem Subst.vliftn_id (n: ℕ): (@id φ).vliftn n = id := by
-  rw [vliftn_eq_iterate_vlift_apply, iterate_vlift_id]
-
-theorem Subst.iterate_vlift_liftn_comm (k n : ℕ) (σ: Subst φ)
-  : Subst.vlift^[k] (σ.liftn n) = (Subst.vlift^[k] σ).liftn n := by
-  induction k generalizing σ with
-  | zero => rfl
-  | succ n I => simp [I, vlift_liftn_comm]
-
-theorem Subst.vliftn_liftn (k n : ℕ) (σ: Subst φ)
-  : (σ.liftn n).vliftn k = (σ.vliftn k).liftn n
-  := by simp [vliftn_eq_iterate_vlift, iterate_vlift_liftn_comm]
-
-theorem Subst.liftn_vliftn (k n : ℕ) (σ: Subst φ)
-  : (σ.vliftn k).liftn n = (σ.liftn n).vliftn k
-  := by simp [vliftn_eq_iterate_vlift, iterate_vlift_liftn_comm]
-
-/-- Substitute the labels in a `Terminator` using `σ` -/
-@[simp]
-def lsubst (σ : Subst φ) : Terminator φ → Terminator φ
-  | Terminator.br n e => (σ n).vsubst e.subst0
-  | Terminator.case e s t => Terminator.case e (lsubst σ.vlift s) (lsubst σ.vlift t)
-
-theorem lsubst_id_apply (t : Terminator φ) : t.lsubst Subst.id = t
-  := by induction t <;> simp [*]
-
-@[simp]
-theorem lsubst_id : @lsubst φ (Subst.id) = id := funext lsubst_id_apply
-
-theorem lsubst_id_apply' (t : Terminator φ) : t.lsubst (λi => Terminator.br i (Term.var 0)) = t
-  := t.lsubst_id_apply
-
-@[simp]
-theorem lsubst_id' : @lsubst φ (λi => Terminator.br i (Term.var 0)) = id := funext lsubst_id_apply'
-
-/-- Create a substitution from a label renaming -/
-def Subst.fromLwk (ρ : ℕ -> ℕ): Subst φ := λn => Terminator.br (ρ n) (Term.var 0)
-
-theorem Subst.vwk_lift_comp_fromLwk (ρ σ) : vwk (Nat.liftWk ρ) ∘ fromLwk σ = @fromLwk φ σ := rfl
-
-theorem Subst.vwk1_comp_fromLwk (σ) : vwk1 ∘ fromLwk σ = @fromLwk φ σ := rfl
-
-@[simp]
-theorem Subst.fromLwk_vlift (ρ) : (@fromLwk φ ρ).vlift = fromLwk ρ := rfl
-
-@[simp]
-theorem Subst.fromLwk_iterate_vlift (n : ℕ) (ρ)
-  : Subst.vlift^[n] (@fromLwk φ ρ) = fromLwk ρ
-  := by induction n <;> simp [fromLwk_vlift, *]
-
-@[simp]
-theorem Subst.fromLwk_vliftn (n ρ) : (@fromLwk φ ρ).vliftn n = fromLwk ρ := by
-  rw [vliftn_eq_iterate_vlift, fromLwk_iterate_vlift]
-
-@[simp]
-theorem Subst.fromLwk_apply (ρ : ℕ -> ℕ) (n : ℕ)
-  : (@fromLwk φ ρ) n = Terminator.br (ρ n) (Term.var 0) := rfl
-
-theorem Subst.fromLwk_lift (ρ) : (@fromLwk φ ρ).lift = fromLwk (Nat.liftWk ρ) := by
-  funext n; cases n <;> rfl
-
-theorem Subst.fromLwk_iterate_lift (n : ℕ) (ρ)
-  : Subst.lift^[n] (@fromLwk φ ρ) = fromLwk (Nat.liftWk^[n] ρ)
-  := by induction n generalizing ρ <;> simp [fromLwk_lift, *]
-
-theorem Subst.fromLwk_liftn (n ρ) : (@fromLwk φ ρ).liftn n = fromLwk (Nat.liftnWk n ρ) := by
-  rw [liftn_eq_iterate_lift, Nat.liftnWk_eq_iterate_liftWk, fromLwk_iterate_lift]
-
-theorem lsubst_fromLwk_apply (ρ : ℕ -> ℕ) (t : Terminator φ)
-  : t.lsubst (Subst.fromLwk ρ) = t.lwk ρ := by
-  induction t generalizing ρ
-  <;> simp [Terminator.lsubst, Terminator.lwk, Term.subst_fromWk_apply, *]
-
-theorem lsubst_fromLwk (ρ : ℕ -> ℕ) : lsubst (Subst.fromLwk ρ) = @lwk φ ρ
-  := funext (lsubst_fromLwk_apply ρ)
-
-theorem lsubst_comp_fromLwk : @lsubst φ ∘ (@Subst.fromLwk φ) = lwk := funext lsubst_fromLwk
-
-theorem lsubst_liftn (n : ℕ) (σ : Subst φ) (t : Terminator φ)
-    : (t.lwk (Nat.liftnWk n Nat.succ)).lsubst (σ.liftn (n + 1))
-      = (t.lsubst (σ.liftn n)).lwk (Nat.liftnWk n Nat.succ)
-  := by induction t generalizing σ n with
-  | br ℓ e =>
-    simp only [lwk, lsubst, Nat.liftnWk, Subst.liftn]
-    split
-    · split
-      · simp [lwk, Nat.liftnWk, *]
-      · rename_i H C; exact (C (Nat.le_step H)).elim
-    · rename_i C
-      simp_arith only [ite_false]
-      rw [Nat.succ_eq_add_one]
-      have h : ℓ - n + 1 + n - (n + 1) = ℓ - n := by
-        rw [Nat.add_assoc, Nat.add_comm 1 n, Nat.add_sub_cancel]
-      rw [h, Terminator.lwk_vsubst, lwk_lwk]
-      congr
-      funext n
-      simp_arith [Nat.liftnWk]
-  | case e s t => simp [Subst.vlift_liftn_comm, *]
-
-theorem lsubst_iterate_lift (n : ℕ) (σ : Subst φ) (t : Terminator φ)
-  : (t.lwk (Nat.liftWk^[n] Nat.succ)).lsubst (Subst.lift^[n + 1] σ)
-    = (t.lsubst (Subst.lift^[n] σ)).lwk (Nat.liftWk^[n] Nat.succ)
-  := by simp only [<-Subst.liftn_eq_iterate_lift, <-Nat.liftnWk_eq_iterate_liftWk, lsubst_liftn]
-
-theorem lsubst_lift (t : Terminator φ) (σ : Subst φ)
-  : (t.lwk Nat.succ).lsubst (σ.lift) = (t.lsubst σ).lwk Nat.succ := t.lsubst_iterate_lift 0 σ
-
-/-- Compose two label-substitutions to yield another -/
-def Subst.comp (σ τ : Subst φ): Subst φ
-  | n => (τ n).lsubst σ.vlift
-
-@[simp]
-theorem Subst.comp_id (σ : Subst φ) : σ.comp Subst.id = σ := by
-  funext n
-  simp only [comp, Terminator.lsubst, Function.comp_apply, vlift, vwk1]
-  rw [<-Terminator.vsubst_fromWk_apply, Terminator.vsubst_vsubst]
-  simp
-
-@[simp]
-theorem Subst.id_comp (σ : Subst φ) : Subst.id.comp σ = σ
-  := by funext n; exact lsubst_id_apply (σ n)
-
-theorem Subst.vlift_comp_liftWk_stepn (σ : Subst φ) (n)
-  : vlift (vwk (Nat.liftWk (· + n)) ∘ σ) = vwk (Nat.liftWk (· + n)) ∘ σ.vlift := by
-  simp only [vlift, vwk1, <-Function.comp.assoc]
-  apply congrArg₂
-  funext i
-  simp only [Function.comp_apply, vwk_vwk]
-  apply congrArg₂
-  funext i
-  simp only [Function.comp_apply, Nat.wkn]
-  cases i <;> simp_arith
-  rfl
-  rfl
-
-theorem Subst.vlift_comp_liftWk_succ (σ : Subst φ)
-  : vlift (vwk (Nat.liftWk Nat.succ) ∘ σ) = vwk (Nat.liftWk Nat.succ) ∘ σ.vlift
-  := rfl
-
-theorem Subst.vlift_comp_wk1 (σ : Subst φ)
-  : vlift (vwk (Nat.wkn 1) ∘ σ) = vwk (Nat.wkn 1) ∘ σ.vlift
-  := Nat.wkn_one ▸ vlift_comp_liftWk_succ σ
-
-theorem vsubst_substn_lsubst_vliftn (t : Terminator φ) (e : Term φ) (σ : Subst φ) (n)
-  : (t.lsubst (σ.vliftn (n + 1))).vsubst (e.substn n)
-  = (t.vsubst (e.substn n)).lsubst (σ.vliftn n)
-  := by induction t generalizing σ e n with
-  | br ℓ e' =>
-    simp only [
-      lsubst, Subst.vliftn, <-Terminator.vsubst_fromWk, Terminator.vsubst_vsubst,
-      Function.comp_apply]
-    congr
-    funext k
-    cases k with
-    | zero => rfl
-    | succ k => simp_arith [Term.Subst.comp, Term.subst, Term.substn, Nat.liftWk]
-  | _ => simp only [vsubst, lsubst,  <-Subst.vliftn_succ, <-Term.substn_succ, *]
-
-theorem vsubst_subst0_lsubst_vlift (t : Terminator φ) (e : Term φ) (σ : Subst φ)
-    : (t.lsubst σ.vlift).vsubst e.subst0 = (t.vsubst e.subst0).lsubst σ := by
-  have h := vsubst_substn_lsubst_vliftn t e σ 0
-  simp only [Term.substn_zero, Subst.vliftn_zero, Subst.vliftn_one, Nat.zero_add] at h
-  exact h
-
-theorem vsubst_substn_vwk (t : Terminator φ) (e : Term φ) (ρ n)
-  : (t.vsubst (e.substn n)).vwk (Nat.liftnWk n ρ)
-  = (t.vwk (Nat.liftnWk (n + 1) ρ)).vsubst ((e.wk (Nat.liftnWk n ρ)).substn n)
-  := by induction t generalizing e ρ n with
-  | br ℓ e' => simp only [vwk, vsubst, Term.subst_substn_wk]
-  | _ => simp [
-    <-Nat.liftnWk_succ_apply',
-    <-Term.substn_succ, Term.subst_substn_wk,
-    Term.wk_wk, Nat.liftnWk_comp_succ, *]
-
-theorem vsubst_subst0_vwk (t : Terminator φ) (e : Term φ) (ρ)
-  : (t.vsubst e.subst0).vwk ρ = (t.vwk (Nat.liftWk ρ)).vsubst (e.wk ρ).subst0 := by
-  have h := vsubst_substn_vwk t e ρ 0
-  simp [Nat.liftnWk_one, Nat.liftnWk_zero, Term.substn_zero] at h
-  exact h
-
-theorem vwk_lsubst (σ ρ) (t : Terminator φ)
-  : (t.lsubst σ).vwk ρ = (t.vwk ρ).lsubst (vwk (Nat.liftWk ρ) ∘ σ)
-  := by induction t generalizing σ ρ with
-  | br ℓ e => simp [vsubst_subst0_vwk]
-  | _ =>
-    simp only [vwk, lsubst, *]
-    congr <;> simp only [
-      Subst.vlift, vwk1, <-Function.comp.assoc, <-vwk_comp, <-Nat.liftWk_comp, Nat.liftWk_comp_succ
-    ]
-
-theorem Subst.vliftn_comp (n : ℕ) (σ τ : Subst φ)
-  : (σ.comp τ).vliftn n = (σ.vliftn n).comp (τ.vliftn n)
-  := by
-  funext m
-  simp only [Function.comp_apply, comp, vlift, vliftn, vwk1, Function.comp_apply]
-  generalize τ m = t
-  rw [vwk_lsubst]
-  simp only [<-Function.comp.assoc, <-vwk_comp, <-Nat.liftWk_comp, Nat.liftWk_comp_succ]
-
-theorem Subst.vlift_comp (σ τ : Subst φ) : (σ.comp τ).vlift = σ.vlift.comp τ.vlift
-  := σ.vliftn_comp 1 τ
-
-theorem lsubst_lsubst (σ τ : Subst φ) (t : Terminator φ)
-  : (t.lsubst τ).lsubst σ = t.lsubst (σ.comp τ)
-  := by induction t generalizing σ τ with
-  | br ℓ e => simp only [lsubst, Subst.comp, vsubst_subst0_lsubst_vlift]
-  | case e s t Is It => simp only [lsubst, Subst.comp, Subst.vlift_comp, *]
-
-theorem lsubst_comp (σ τ : Subst φ)
-  : Terminator.lsubst (σ.comp τ) = Terminator.lsubst σ ∘ Terminator.lsubst τ
-  := Eq.symm $ funext $ lsubst_lsubst σ τ
-
-theorem Subst.liftn_comp (n : ℕ) (σ τ : Subst φ) : (σ.comp τ).liftn n = (σ.liftn n).comp (τ.liftn n)
-  := by
-  funext k
-  simp only [liftn, comp]
-  split
-  case isTrue h => simp [liftn, vlift, h]
-  case isFalse h =>
-    simp only [vlift, ←lsubst_fromLwk_apply, lsubst_lsubst]
-    congr
-    funext k
-    simp only [comp, vlift, vwk1, vwk_lift_comp_fromLwk, Function.comp_apply, lsubst_fromLwk_apply,
-      lsubst, Term.subst0_var0, liftn, Nat.add_sub_cancel, vwk_vwk, vsubst_fromWk_apply]
-    rw [ite_cond_eq_false]
-    simp only [vwk_lwk]
-    congr
-    funext k
-    cases k <;> rfl
-    simp_arith
-
-theorem Subst.lift_comp (σ τ : Subst φ) : (σ.comp τ).lift = σ.lift.comp τ.lift := by
-  have h := Subst.liftn_comp 1 σ τ
-  simp only [Subst.liftn_one] at h
-  exact h
-
-end Terminator
-
-/-- Substitute the free labels in this basic block -/
-def Block.lsubst (σ : Terminator.Subst φ) (β : Block φ) : Block φ where
-  body := β.body
-  terminator := β.terminator.lsubst (σ.vliftn β.body.num_defs)
-
-/-- Substitute the free labels in this region -/
-def BBRegion.lsubst (σ : Terminator.Subst φ) : BBRegion φ → BBRegion φ
-  | cfg β n f => cfg (β.lsubst (σ.liftn n)) n
-    (λ i => (f i).lsubst ((σ.liftn n).vliftn (β.body.num_defs + 1)))
-
-/-- Substitute the free labels in this control-flow graph -/
-def BBCFG.lsubst (σ : Terminator.Subst φ) (cfg : BBCFG φ) : BBCFG φ where
-  length := cfg.length
-  targets := λi => (cfg.targets i).lsubst σ
-
-/-- Substitute the free labels in this region -/
-def TRegion.lsubst (σ : Terminator.Subst φ) : TRegion φ → TRegion φ
-  | let1 e t => let1 e (t.lsubst σ.vlift)
-  | let2 e t => let2 e (t.lsubst (σ.vliftn 2))
-  | cfg β n f => cfg (β.lsubst (σ.liftn n)) n (λ i => (f i).lsubst (σ.liftn n).vlift)
-
-/-- Substitute the free labels in this control-flow graph -/
-def TCFG.lsubst (σ : Terminator.Subst φ) (cfg : TCFG φ) : TCFG φ where
-  length := cfg.length
-  targets := λi => (cfg.targets i).lsubst σ
-
-/-! ### Region substitutions
- -/
-namespace Region
-
-/-- A substitution mapping labels to regions -/
-def Subst (φ : Type _) := ℕ → Region φ -- TODO: Region.Subst?
-
-/-- The identity substitution, which maps labels to themselves -/
-def Subst.id : Subst φ := λn => Region.br n (Term.var 0)
-
-theorem Subst.id_apply (n : ℕ) : @Subst.id φ n = Region.br n (Term.var 0) := rfl
-
-/-- Lift a substitution under a label binder -/
-def Subst.lift (σ : Subst φ) : Subst φ
-  | 0 => Region.br 0 (Term.var 0)
-  | n + 1 => (σ n).lwk Nat.succ
-
-/-- Lift a substitution under `n` label binders -/
-def Subst.liftn (n : ℕ) (σ : Subst φ) : Subst φ
-  := λm => if m < n then Region.br m (Term.var 0) else (σ (m - n)).lwk (λv => v + n)
-
-@[simp]
-theorem Subst.liftn_zero (σ : Subst φ) : σ.liftn 0 = σ := by
-  funext n
-  simp only [liftn]
-  split
-  · rename_i H; cases H
-  · exact (σ n).lwk_id
-
-theorem Subst.liftn_one (σ : Subst φ) : σ.liftn 1 = σ.lift := by funext m; cases m <;> rfl
-
-theorem Subst.liftn_succ (n) (σ: Subst φ) : σ.liftn n.succ = (σ.liftn n).lift := by
-  induction n with
-  | zero => rw [σ.liftn_one, σ.liftn_zero]
-  | succ n I => -- TODO: I'm sure this can be made _much_ cleaner...
-    funext m
-    rw [I]
-    simp only [lift]
-    split
-    · rfl
-    · simp only [liftn]
-      split
-      · split
-        · rfl
-        · split
-          · rfl
-          · rename_i H C; exact (C (Nat.lt_of_succ_lt_succ (Nat.lt_of_succ_lt_succ H))).elim
-      · split
-        · rename_i H; simp_arith at H
-        · split
-          · rename_i C H; exact (C (Nat.succ_lt_succ (Nat.succ_lt_succ H))).elim
-          · simp only [Region.lwk_lwk]
-            apply congr
-            apply congrArg
-            funext v
-            simp_arith
-            simp_arith
-
-theorem Subst.liftn_eq_iterate_lift_apply (n: ℕ) (σ: Subst φ) : σ.liftn n = (Subst.lift^[n] σ) := by
-  induction n with
-  | zero => exact σ.liftn_zero
-  | succ n => simp only [Function.iterate_succ_apply', Subst.liftn_succ, *]
-
-theorem Subst.liftn_eq_iterate_lift (n: ℕ) : Subst.liftn n = (@Subst.lift φ)^[n] := by
-  funext σ
-  rw [liftn_eq_iterate_lift_apply]
-
-theorem Subst.liftn_succ' (n) (σ: Subst φ) : σ.liftn n.succ = σ.lift.liftn n := by
-  simp [liftn_eq_iterate_lift]
-
-@[simp]
-theorem Subst.lift_id : (@id φ).lift = id := by funext n; cases n <;> rfl
-
-@[simp]
-theorem Subst.iterate_lift_id : (n: ℕ) -> Subst.lift^[n] (@id φ) = id
-  | 0 => rfl
-  | n + 1 => by simp [lift_id, iterate_lift_id n]
-
-@[simp]
-theorem Subst.liftn_id (n: ℕ): (@id φ).liftn n = id := by
-  rw [liftn_eq_iterate_lift_apply, iterate_lift_id]
-
-theorem Subst.liftn_add (n m: ℕ) : Subst.liftn (m + n) = (@Subst.liftn α m) ∘ (@Subst.liftn α n)
-  := by simp [liftn_eq_iterate_lift, Function.iterate_add]
-
-theorem Subst.liftn_liftn (n m: ℕ) (σ: Subst φ): (σ.liftn n).liftn m = σ.liftn (m + n)
-  := by simp [liftn_add]
-
-theorem Subst.lift_succ (σ : Subst φ) (i : ℕ) : σ.lift (i + 1) = (σ i).lwk Nat.succ := rfl
-
-/-- Lift a substitution under a variable binder -/
-def Subst.vlift (σ : Subst φ) : Subst φ := vwk1 ∘ σ
-
-@[simp]
-theorem Subst.vlift_id : (@id φ).vlift = id := by funext v; cases v <;> rfl
-
-theorem Subst.vlift_lift_comm (σ : Subst σ) : σ.lift.vlift = σ.vlift.lift := by
-  funext n
-  cases n with
-  | zero => rfl
-  | succ n => simp [Subst.vlift, vwk1, lift, vwk_lwk]
-
-theorem Subst.vlift_lift_comp_comm : Subst.vlift ∘ (@Subst.lift φ) = Subst.lift ∘ Subst.vlift
-  := funext Subst.vlift_lift_comm
-
-theorem Subst.vlift_liftn_comm (n : ℕ) (σ : Subst σ) : (σ.liftn n).vlift = σ.vlift.liftn n := by
-  induction n generalizing σ with
-  | zero => simp
-  | succ _ I => rw [liftn_succ, vlift_lift_comm, I, liftn_succ]
-
-/-- Lift a substitution under `n` variable binders -/
-def Subst.vliftn (n : ℕ) (σ : Subst φ) : Subst φ
-  := Region.vwk (Nat.liftWk (λi => i + n)) ∘ σ
-
-@[simp]
-theorem Subst.vliftn_zero (σ : Subst φ) : σ.vliftn 0 = σ := by
-  funext n
-  simp [vliftn]
-
-theorem Subst.vliftn_one (σ : Subst φ) : σ.vliftn 1 = σ.vlift := by
-  funext n
-  simp [vliftn, vlift, vwk1]
-
-theorem Subst.vliftn_succ (σ : Subst φ) (i : ℕ) : σ.vliftn (i + 1) = (σ.vliftn i).vlift := by
-  funext ℓ
-  simp only [vliftn, vwk1, Function.comp_apply, vlift, vwk_vwk]
-  congr
-  funext n
-  cases n <;> rfl
-
-theorem Subst.vliftn_two (σ : Subst φ) : σ.vliftn 2 = σ.vlift.vlift := by
-  rw [Subst.vliftn_succ, Subst.vliftn_succ]; simp
-
-theorem Subst.vliftn_eq_iterate_vlift_apply (n: ℕ) (σ: Subst φ) : σ.vliftn n = (Subst.vlift^[n] σ)
-  := by induction n with
-  | zero => exact σ.vliftn_zero
-  | succ n => simp only [Function.iterate_succ_apply', Subst.vliftn_succ, *]
-
-theorem Subst.vliftn_eq_iterate_vlift (n: ℕ) : Subst.vliftn n = (@Subst.vlift φ)^[n] := by
-  funext σ
-  rw [vliftn_eq_iterate_vlift_apply]
-
-theorem Subst.vliftn_succ' (σ : Subst φ) (i : ℕ) : σ.vliftn (i + 1) = σ.vlift.vliftn i
-  := by simp [vliftn_eq_iterate_vlift]
-
-theorem Subst.vliftn_add (σ : Subst φ) (n m: ℕ) : σ.vliftn (n + m) = (σ.vliftn m).vliftn n := by
-  funext k
-  simp [vliftn_eq_iterate_vlift, Function.iterate_add_apply]
-
-theorem Subst.iterate_vlift_id : (n: ℕ) -> Subst.vlift^[n] (@id φ) = id
-  | 0 => rfl
-  | n + 1 => by simp [Subst.vlift_id, iterate_vlift_id n]
-
-@[simp]
-theorem Subst.vliftn_id (n: ℕ): (@id φ).vliftn n = id := by
-  rw [vliftn_eq_iterate_vlift_apply, iterate_vlift_id]
-
-theorem Subst.iterate_vlift_liftn_comm (k n : ℕ) (σ: Subst φ)
-  : Subst.vlift^[k] (σ.liftn n) = (Subst.vlift^[k] σ).liftn n := by
-  induction k generalizing σ with
-  | zero => rfl
-  | succ n I => simp [I, vlift_liftn_comm]
-
-theorem Subst.vliftn_liftn (k n : ℕ) (σ: Subst φ)
-  : (σ.liftn n).vliftn k = (σ.vliftn k).liftn n
-  := by simp [vliftn_eq_iterate_vlift, iterate_vlift_liftn_comm]
-
-/-- Substitute the labels in a `Region` using `σ` -/
-@[simp]
-def lsubst (σ : Subst φ) : Region φ → Region φ
-  | br n e => (σ n).vsubst e.subst0
-  | case e s t => case e (lsubst σ.vlift s) (lsubst σ.vlift t)
-  | let1 e t => let1 e (lsubst σ.vlift t)
-  | let2 e t => let2 e (lsubst (σ.vliftn 2) t)
-  | cfg β n f => cfg (lsubst (σ.liftn n) β) n (λ i => lsubst (σ.liftn n).vlift (f i))
-
-theorem lsubst_id_apply (t : Region φ) : t.lsubst Subst.id = t
-  := by induction t <;> simp [*]
-
-@[simp]
-theorem lsubst_id : @lsubst φ (Subst.id) = id := funext lsubst_id_apply
-
-theorem lsubst_id_apply' (t : Region φ) : t.lsubst (λi => Region.br i (Term.var 0)) = t
-  := t.lsubst_id_apply
-
-@[simp]
-theorem lsubst_id' : @lsubst φ (λi => Region.br i (Term.var 0)) = id := funext lsubst_id_apply'
-
-theorem lsubst_id_eq {t : Region φ} {σ : Subst φ} (hσ : σ = Subst.id)
-  : t.lsubst σ = t := by cases hσ; simp
-
-theorem lsubst_cfg
-  : @lsubst φ σ (cfg β n G) = cfg (lsubst (σ.liftn n) β) n (lsubst (σ.liftn n).vlift ∘ G)
-  := rfl
-
-theorem lsubst_cfg1
-  : @lsubst φ σ (cfg β 1 (Fin.elim1 G))
-  = cfg (lsubst σ.lift β) 1 (Fin.elim1 $ lsubst σ.lift.vlift G) := by
-  simp only [lsubst, cfg.injEq, heq_eq_eq, true_and, Subst.liftn_one]
-  funext i; cases i using Fin.elim1; rfl
-
-/-- Create a substitution from a label renaming -/
-def Subst.fromLwk (ρ : ℕ -> ℕ): Subst φ := λn => Region.br (ρ n) (Term.var 0)
-
-@[simp]
-theorem Subst.vwk_lift_comp_fromLwk (ρ σ) : vwk (Nat.liftWk ρ) ∘ fromLwk σ = @fromLwk φ σ := rfl
-
-@[simp]
-theorem Subst.vwk1_comp_fromLwk (σ) : vwk1 ∘ fromLwk σ = @fromLwk φ σ := rfl
-
-@[simp]
-theorem Subst.vwk_lift_comp_id (ρ) : vwk (Nat.liftWk ρ) ∘ Subst.id = @Subst.id φ := rfl
-
-@[simp]
-theorem Subst.vsubst_lift_comp_id (σ : Term.Subst φ) : vsubst σ.lift ∘ Subst.id = Subst.id := rfl
-
-@[simp]
-theorem Subst.fromLwk_vlift (ρ) : (@fromLwk φ ρ).vlift = fromLwk ρ := rfl
-
-@[simp]
-theorem Subst.fromLwk_iterate_vlift (n : ℕ) (ρ)
-  : Subst.vlift^[n] (@fromLwk φ ρ) = fromLwk ρ
-  := by induction n <;> simp [fromLwk_vlift, *]
-
-@[simp]
-theorem Subst.fromLwk_vliftn (n ρ) : (@fromLwk φ ρ).vliftn n = fromLwk ρ := by
-  rw [vliftn_eq_iterate_vlift, fromLwk_iterate_vlift]
-
-@[simp]
-theorem Subst.fromLwk_apply (ρ : ℕ -> ℕ) (n : ℕ)
-  : (@fromLwk φ ρ) n = Region.br (ρ n) (Term.var 0) := rfl
-
-theorem Subst.fromLwk_lift (ρ) : (@fromLwk φ ρ).lift = fromLwk (Nat.liftWk ρ) := by
-  funext n; cases n <;> rfl
-
-theorem Subst.fromLwk_iterate_lift (n : ℕ) (ρ)
-  : Subst.lift^[n] (@fromLwk φ ρ) = fromLwk (Nat.liftWk^[n] ρ)
-  := by induction n generalizing ρ <;> simp [fromLwk_lift, *]
-
-theorem Subst.fromLwk_liftn (n ρ) : (@fromLwk φ ρ).liftn n = fromLwk (Nat.liftnWk n ρ) := by
-  rw [liftn_eq_iterate_lift, Nat.liftnWk_eq_iterate_liftWk, fromLwk_iterate_lift]
-
-theorem lsubst_fromLwk_apply (ρ : ℕ -> ℕ) (t : Region φ)
-  : t.lsubst (Subst.fromLwk ρ) = t.lwk ρ := by
-  induction t generalizing ρ
-  <;> simp [Region.lsubst, Region.lwk, Term.subst_fromWk_apply, Subst.fromLwk_liftn, *]
-
-theorem lsubst_fromLwk (ρ : ℕ -> ℕ) : lsubst (Subst.fromLwk ρ) = @lwk φ ρ
-  := funext (lsubst_fromLwk_apply ρ)
-
-theorem lsubst_comp_fromLwk : @lsubst φ ∘ (@Subst.fromLwk φ) = lwk := funext lsubst_fromLwk
-
-theorem lsubst_liftn (n : ℕ) (σ : Subst φ) (t : Region φ)
-    : (t.lwk (Nat.liftnWk n Nat.succ)).lsubst (σ.liftn (n + 1))
-      = (t.lsubst (σ.liftn n)).lwk (Nat.liftnWk n Nat.succ)
-  := by induction t generalizing σ n with
-  | br ℓ e =>
-    simp only [lwk, lsubst, Nat.liftnWk, Subst.liftn]
-    split
-    · split
-      · simp [lwk, Nat.liftnWk, *]
-      · rename_i H C; exact (C (Nat.le_step H)).elim
-    · rename_i C
-      simp_arith only [ite_false]
-      rw [Nat.succ_eq_add_one]
-      have h : ℓ - n + 1 + n - (n + 1) = ℓ - n := by
-        rw [Nat.add_assoc, Nat.add_comm 1 n, Nat.add_sub_cancel]
-      rw [h, Region.lwk_vsubst, lwk_lwk]
-      congr
-      funext n
-      simp_arith [Nat.liftnWk]
-  | cfg β k G Iβ IG => simp only [
-    Subst.vlift_liftn_comm, lsubst, lwk, Subst.liftn_liftn,
-    <-Nat.add_assoc, <-Nat.liftnWk_add_apply, *]
-  | _ => simp [Subst.vlift_liftn_comm, Subst.vliftn_liftn, *]
-
-theorem lsubst_iterate_lift (n : ℕ) (σ : Subst φ) (t : Region φ)
-  : (t.lwk (Nat.liftWk^[n] Nat.succ)).lsubst (Subst.lift^[n + 1] σ)
-    = (t.lsubst (Subst.lift^[n] σ)).lwk (Nat.liftWk^[n] Nat.succ)
-  := by simp only [<-Subst.liftn_eq_iterate_lift, <-Nat.liftnWk_eq_iterate_liftWk, lsubst_liftn]
-
-theorem lsubst_lift (t : Region φ) (σ : Subst φ)
-  : (t.lwk Nat.succ).lsubst (σ.lift) = (t.lsubst σ).lwk Nat.succ := t.lsubst_iterate_lift 0 σ
-
-/-- Compose two label-substitutions to yield another -/
-def Subst.comp (σ τ : Subst φ): Subst φ
-  | n => (τ n).lsubst σ.vlift
-
-@[simp]
-theorem Subst.comp_id (σ : Subst φ) : σ.comp Subst.id = σ := by
-  funext n
-  simp only [comp, Region.lsubst, Function.comp_apply, vlift, vwk1]
-  rw [<-Region.vsubst_fromWk_apply, <-Region.vsubst_comp_apply]
-  simp
-
-@[simp]
-theorem Subst.id_comp (σ : Subst φ) : Subst.id.comp σ = σ
-  := by funext n; exact lsubst_id_apply (σ n)
-
-theorem Subst.vlift_comp_liftWk_stepn (σ : Subst φ) (n)
-    : vlift (vwk (Nat.liftWk (· + n)) ∘ σ) = vwk (Nat.liftWk (· + n)) ∘ σ.vlift := by
-  simp only [vlift, vwk1, <-Function.comp.assoc]
-  apply congrArg₂
-  funext i
-  simp only [Function.comp_apply, vwk_vwk]
-  apply congrArg₂
-  funext i
-  simp only [Function.comp_apply, Nat.wkn]
-  cases i <;> simp_arith
-  rfl
-  rfl
-
-theorem Subst.vlift_comp_liftWk_succ (σ : Subst φ)
-  : vlift (vwk (Nat.liftWk Nat.succ) ∘ σ) = vwk (Nat.liftWk Nat.succ) ∘ σ.vlift
-  := rfl
-
-theorem Subst.vlift_comp_wk1 (σ : Subst φ)
-  : vlift (vwk (Nat.wkn 1) ∘ σ) = vwk (Nat.wkn 1) ∘ σ.vlift
-  := Nat.wkn_one ▸ vlift_comp_liftWk_succ σ
-
-theorem vsubst_substn_lsubst_vliftn (t : Region φ) (e : Term φ) (σ : Subst φ) (n)
-  : (t.lsubst (σ.vliftn (n + 1))).vsubst (e.substn n)
-  = (t.vsubst (e.substn n)).lsubst (σ.vliftn n)
-  := by induction t generalizing σ e n with
-  | br ℓ e' =>
-    simp only [
-      lsubst, Subst.vliftn, <-Region.vsubst_fromWk, <-Region.vsubst_comp_apply,
-      Function.comp_apply]
-    congr
-    funext k
-    cases k with
-    | zero => rfl
-    | succ k => simp_arith [Term.Subst.comp, Term.subst, Term.substn, Nat.liftWk]
-  | _ => simp only [
-    vsubst, lsubst,  <-Subst.vliftn_succ, <-Term.substn_succ,
-    <-Subst.vliftn_add, <-Nat.add_assoc, <-Term.substn_add_right,
-    <-Subst.vliftn_liftn, *
-  ]
-
-theorem vsubst_subst0_lsubst_vlift (t : Region φ) (e : Term φ) (σ : Subst φ)
-    : (t.lsubst σ.vlift).vsubst e.subst0 = (t.vsubst e.subst0).lsubst σ := by
-  have h := vsubst_substn_lsubst_vliftn t e σ 0
-  simp only [Term.substn_zero, Subst.vliftn_zero, Subst.vliftn_one, Nat.zero_add] at h
-  exact h
-
-theorem vsubst_substn_vwk (t : Region φ) (e : Term φ) (ρ n)
-  : (t.vsubst (e.substn n)).vwk (Nat.liftnWk n ρ)
-  = (t.vwk (Nat.liftnWk (n + 1) ρ)).vsubst ((e.wk (Nat.liftnWk n ρ)).substn n)
-  := by induction t generalizing e ρ n <;> simp [
-        <-Nat.liftnWk_succ_apply', ← Nat.liftnWk_add_apply,
-        <-Term.substn_succ, Term.subst_substn_wk,
-        Term.wk_wk, Nat.liftnWk_comp_succ,  ← Term.substn_add_right,
-        <-Nat.add_assoc, Nat.liftnWk_comp_add_right, *
-      ]
-
-theorem vsubst_subst0_vwk (t : Region φ) (e : Term φ) (ρ)
-  : (t.vsubst e.subst0).vwk ρ = (t.vwk (Nat.liftWk ρ)).vsubst (e.wk ρ).subst0 := by
-  have h := vsubst_substn_vwk t e ρ 0
-  simp [Nat.liftnWk_one, Nat.liftnWk_zero, Term.substn_zero] at h
-  exact h
-
-theorem Subst.vwk_liftWk_comp_liftn (σ : Subst φ) (ρ)
-    : vwk (Nat.liftWk ρ) ∘ σ.liftn n = liftn n (vwk (Nat.liftWk ρ) ∘ σ) := by
-  funext k
-  simp only [Function.comp_apply, liftn]
-  split
-  rfl
-  rw [lwk_vwk]
-
-theorem Subst.vwk_liftWk_liftWk_comp_vlift (σ : Subst φ) (ρ)
-    : vwk (Nat.liftWk (Nat.liftWk ρ)) ∘ σ.vlift = vlift (vwk (Nat.liftWk ρ) ∘ σ) := by
-  simp only [vlift, vwk1, ← Function.comp.assoc, ← vwk_comp, ← Nat.liftWk_comp, Nat.liftWk_comp_succ]
-
-theorem Subst.vwk_liftWk_liftnWk_comp_vliftn (n : ℕ) (σ : Subst φ) (ρ)
-    : vwk (Nat.liftWk (Nat.liftnWk n ρ)) ∘ σ.vliftn n = vliftn n (vwk (Nat.liftWk ρ) ∘ σ) := by
-  simp only [vliftn, ← Function.comp.assoc, ← vwk_comp, ← Nat.liftWk_comp, Nat.liftnWk_comp_add]
-
-theorem vwk_lsubst (σ ρ) (t : Region φ)
-  : (t.lsubst σ).vwk ρ = (t.vwk ρ).lsubst (vwk (Nat.liftWk ρ) ∘ σ)
-  := by induction t generalizing σ ρ with
-  | br ℓ e => simp [vsubst_subst0_vwk]
-  | _ =>
-    simp only [
-      vwk, lsubst,
-      Subst.vwk_liftWk_liftWk_comp_vlift, Subst.vwk_liftWk_liftnWk_comp_vliftn,
-      Subst.vwk_liftWk_comp_liftn, *]
-
-theorem vwk1_lsubst (σ) (t : Region φ)
-  : (t.lsubst σ).vwk1 = t.vwk1.lsubst (vwk2 ∘ σ)
-  := by rw [vwk1, vwk_lsubst, vwk2, Nat.liftnWk_two]; rfl
-
-theorem Subst.vliftn_comp (n : ℕ) (σ τ : Subst φ)
-  : (σ.comp τ).vliftn n = (σ.vliftn n).comp (τ.vliftn n)
-  := by
-  funext m
-  simp only [Function.comp_apply, comp, vlift, vliftn, vwk1, Function.comp_apply]
-  generalize τ m = t
-  rw [vwk_lsubst]
-  simp only [<-Function.comp.assoc, <-vwk_comp, <-Nat.liftWk_comp, Nat.liftWk_comp_succ]
-
-theorem Subst.vlift_comp (σ τ : Subst φ) : (σ.comp τ).vlift = σ.vlift.comp τ.vlift
-  := σ.vliftn_comp 1 τ
-
-theorem Subst.lwk_comp_vlift (ρ) (σ : Subst φ) : lwk ρ ∘ σ.vlift = vlift (lwk ρ ∘ σ)
-  := by simp only [vlift, vwk1, <-Function.comp.assoc, vwk_comp_lwk]
-
-theorem Subst.lwk_comp_vliftn (ρ) (σ : Subst φ) (n) : lwk ρ ∘ σ.vliftn n = vliftn n (lwk ρ ∘ σ)
-  := by simp only [vliftn, <-Function.comp.assoc, vwk_comp_lwk]
-
-theorem Subst.vlift_comp_lwk (σ : Subst φ) (ρ) : vlift (σ ∘ ρ) = σ.vlift ∘ ρ := rfl
-
-theorem Subst.vliftn_comp_lwk (σ : Subst φ) (ρ) (n) : vliftn n (σ ∘ ρ) = σ.vliftn n ∘ ρ := rfl
-
-theorem Subst.liftn_comp_lwk (σ : Subst φ) (ρ) (n) : liftn n (σ ∘ ρ) = σ.liftn n ∘ Nat.liftnWk n ρ
-  := by funext i; simp only [liftn, Function.comp_apply, Nat.liftnWk]; split <;> simp_arith
-
-theorem Subst.liftn_lwk_comp (σ : Subst φ) (ρ) (n)
-    : liftn n (lwk ρ ∘ σ) = lwk (Nat.liftnWk n ρ) ∘ σ.liftn n := by
-  funext i
-  simp only [liftn, Function.comp_apply, lwk, Nat.liftnWk]
-  split
-  · simp [Nat.liftnWk, *]
-  · rw [lwk_lwk, lwk_lwk, Nat.liftnWk_comp_add]
-
-theorem lwk_lsubst (σ ρ) (t : Region φ)
-  : (t.lsubst σ).lwk ρ = t.lsubst (lwk ρ ∘ σ)
-  := by induction t generalizing σ ρ with
-  | br ℓ e => simp only [lsubst, Function.comp_apply, lwk_vsubst]
-  | _ => simp [Subst.lwk_comp_vlift, Subst.lwk_comp_vliftn, Subst.liftn_lwk_comp , *]
-
-theorem lsubst_lwk (σ ρ) (t : Region φ)
-  : (t.lwk ρ).lsubst σ = t.lsubst (σ ∘ ρ) := by
-  induction t generalizing σ ρ with
-  | br ℓ e => rfl
-  | _ => simp [Subst.vlift_comp_lwk, Subst.vliftn_comp_lwk, Subst.liftn_comp_lwk, *]
-
-theorem Subst.liftn_comp_add (n) (σ : Subst φ) : σ.liftn n ∘ (· + n) = lwk (· + n) ∘ σ := by
-  funext i; simp [liftn]
-
-theorem Subst.liftn_comp (n : ℕ) (σ τ : Subst φ) : (σ.comp τ).liftn n = (σ.liftn n).comp (τ.liftn n)
-  := by
-  funext k
-  simp only [liftn, comp]
-  split
-  case isTrue h => simp [liftn, vlift, h]
-  case isFalse h =>
-    rw [lwk_lsubst, lsubst_lwk]
-    congr
-    rw [lwk_comp_vlift, vlift, vlift, Function.comp.assoc, liftn_comp_add]
-
-theorem Subst.lift_comp (σ τ : Subst φ) : (σ.comp τ).lift = σ.lift.comp τ.lift := by
-  have h := Subst.liftn_comp 1 σ τ
-  simp only [Subst.liftn_one] at h
-  exact h
-
-theorem lsubst_lsubst (σ τ : Subst φ) (t : Region φ)
-  : (t.lsubst τ).lsubst σ = t.lsubst (σ.comp τ)
-  := by induction t generalizing σ τ with
-  | br ℓ e => simp only [lsubst, Subst.comp, vsubst_subst0_lsubst_vlift]
-  | _ => simp only [lsubst, Subst.comp, Subst.vlift_comp, Subst.vliftn_comp, Subst.liftn_comp, *]
-
-theorem lsubst_comp (σ τ : Subst φ)
-  : Region.lsubst (σ.comp τ) = Region.lsubst σ ∘ Region.lsubst τ
-  := Eq.symm $ funext $ lsubst_lsubst σ τ
-
-/-- Substitute the labels in a `Region` using `σ` and let-bindings -/
-@[simp]
-def llsubst (σ : Subst φ) : Region φ → Region φ
-  := lsubst (let1 (Term.var 0) ∘ σ.vlift)
-
-/-- Compose two label-substitutions via let-bindings to yield another -/
-def Subst.lcomp (σ τ : Subst φ): Subst φ
-  | n => (τ n).llsubst σ.vlift
-
-theorem Subst.vlift_let1_zero (σ : Subst φ)
-    : vlift (let1 (Term.var 0) ∘ σ.vlift) = let1 (Term.var 0) ∘ σ.vlift.vlift :=
-  by funext k; simp [vlift, vwk1, vwk_vwk, <-Nat.liftWk_comp, Nat.liftWk_comp_succ]
-
-theorem Subst.vliftn_let1_zero (σ : Subst φ)
-    : vliftn n (let1 (Term.var 0) ∘ σ.vlift) = let1 (Term.var 0) ∘ (σ.vliftn n).vlift :=
-  by induction n with
-  | zero => simp
-  | succ n I => rw [vliftn_succ, I, vlift_let1_zero, vliftn_succ]
-
-theorem llsubst_lcomp (σ τ : Subst φ) : llsubst (σ.lcomp τ) = llsubst σ ∘ llsubst τ := by
-  simp only [llsubst, <-lsubst_comp]
-  apply congrArg
-  funext k
-  simp only [Subst.vlift, vwk1, Function.comp_apply, Subst.lcomp, llsubst, Subst.comp, lsubst, let1.injEq,
-    true_and]
-  rw [vwk_lsubst]
-  congr
-  funext k
-  simp only [Function.comp_apply, vwk, Term.wk, Nat.liftWk_zero, let1.injEq, true_and, vwk_vwk]
-  congr
-  simp only [<-Nat.liftWk_comp, Nat.liftWk_comp_succ, <-Function.comp.assoc]
-  rw [Function.comp.assoc, Nat.liftWk_comp_succ, Function.comp.assoc]
-
-theorem llsubst_llsubst (σ τ : Subst φ) (t : Region φ)
-  : (t.llsubst τ).llsubst σ = t.llsubst (σ.lcomp τ)
-  := by rw [llsubst_lcomp]; simp
-
-def let1V0 (r : Region φ) : Region φ := (r.vwk (Nat.liftWk Nat.succ)).let1 (Term.var 0)
-
-theorem lsubst_let1V0_comp (σ : Subst φ) (r : Region φ)
-  : (r.lsubst (let1V0 ∘ σ)) = r.llsubst σ
-  := rfl
-
-def let1Br : Subst φ := λℓ => (br ℓ (Term.var 0)).let1 (Term.var 0)
-
-theorem Subst.let1V0_comp_id : @let1V0 φ ∘ id = let1Br := rfl
-
-theorem lwk_lsubst_swap (σ σ' : Subst φ) (ρ ρ') (r : Region φ)
-  (h : lwk ρ ∘ σ = σ' ∘ ρ')
-  : (r.lsubst σ).lwk ρ = (r.lwk ρ').lsubst σ'
-  := by rw [lwk_lsubst, lsubst_lwk, h]
-
-theorem lsubst_lwk_swap (σ σ' : Subst φ) (ρ ρ') (r : Region φ)
-  (h : σ ∘ ρ = lwk ρ' ∘ σ')
-  : (r.lwk ρ).lsubst σ = (r.lsubst σ').lwk ρ'
-  := by rw [lwk_lsubst, lsubst_lwk, h]
-
-theorem lwk_lsubst_comm (σ : Subst φ) (ρ) (r : Region φ)
-  (h : lwk ρ ∘ σ = σ ∘ ρ)
-  : (r.lsubst σ).lwk ρ = (r.lwk ρ).lsubst σ
-  := lwk_lsubst_swap σ σ ρ ρ r h
-
-theorem lsubst_lwk_comm (σ : Subst φ) (ρ) (r : Region φ)
-  (h : σ ∘ ρ = lwk ρ ∘ σ)
-  : (r.lwk ρ).lsubst σ = (r.lsubst σ).lwk ρ
-  := lsubst_lwk_swap σ σ ρ ρ r h
-
-theorem Subst.liftn_comp_toNatWk {ρ : Fin k → Fin n}
-  : (@liftn φ n σ) ∘ (Fin.toNatWk ρ) = (lwk $ Fin.toNatWk ρ) ∘ (@liftn φ k σ) := by
-  funext i
-  simp only [Function.comp_apply, liftn, Fin.toNatWk]
-  split
-  case isTrue h => simp [Fin.toNatWk, h]
-  case isFalse h =>
-    simp [Nat.sub_add_cancel (Nat.le_of_not_lt h), h, lwk_lwk, Fin.toNatWk_comp_add]
-
-theorem lsubst_liftn_lwk_toNatWk {ρ : Fin k → Fin n}
-    : (lsubst (@Subst.liftn φ n σ) (lwk (Fin.toNatWk ρ) r))
-      = (lwk (Fin.toNatWk ρ) (lsubst (Subst.liftn k σ) r)) := by
-  apply lsubst_lwk_swap
-  apply Subst.liftn_comp_toNatWk
-
-theorem lsubst_liftn_comp_lwk_toNatWk {ρ : Fin k → Fin n}
-    : (lsubst (Subst.liftn n σ) ∘ lwk (Fin.toNatWk ρ))
-      = (lwk (Fin.toNatWk ρ) ∘ lsubst (Subst.liftn k σ)) := by
-  funext r
-  apply lsubst_liftn_lwk_toNatWk
-
-theorem vsubst_lift_lift_comp_vwk1 {ρ : Term.Subst φ}
-  : (vsubst ρ.lift.lift ∘ vwk1) = (vwk1 ∘ vsubst ρ.lift) := by
-  simp only [vwk1, <-vsubst_fromWk, vsubst_comp]
-  apply congrArg
-  funext k
-  cases k with
-  | zero => rfl
-  | succ =>
-    simp only [Term.Subst.comp, Term.subst, Nat.liftWk_succ, Nat.succ_eq_add_one,
-      Term.Subst.lift_succ, Term.wk_wk, Term.subst_fromWk, Nat.liftWk_succ_comp_succ]
-    rfl
-
-theorem vsubst_lift₂_vwk1 {ρ : Term.Subst φ} {r : Region φ}
-  : r.vwk1.vsubst ρ.lift.lift = (r.vsubst ρ.lift).vwk1 := congrFun vsubst_lift_lift_comp_vwk1 r
-
-theorem vsubst_lift_lift_comp_vlift {ρ : Term.Subst φ} {σ : Subst φ}
-  : (vsubst ρ.lift.lift ∘ σ.vlift) = Subst.vlift (vsubst ρ.lift ∘ σ) := by
-  rw [Subst.vlift, <-Function.comp.assoc, vsubst_lift_lift_comp_vwk1]; rfl
-
-theorem Subst.vsubst_lift_comp_liftn (σ : Subst φ) (ρ : Term.Subst φ)
-    : vsubst ρ.lift ∘ σ.liftn n = liftn n (vsubst ρ.lift ∘ σ) := by
-  funext k
-  simp only [Function.comp_apply, liftn]
-  split
-  rfl
-  rw [vsubst_lwk]
-
-theorem vsubst_lsubst (σ ρ) (t : Region φ)
-  : (t.lsubst σ).vsubst ρ = (t.vsubst ρ).lsubst (vsubst ρ.lift ∘ σ)
-  := by induction t generalizing σ ρ with
-  | br ℓ e =>
-    simp only [lsubst, vsubst_vsubst, Function.comp_apply]
-    congr
-    funext k
-    cases k <;> simp [Term.Subst.comp]
-  | _ =>
-    simp only [
-      vsubst, lsubst, Term.Subst.liftn_two, Subst.vliftn_two, vsubst_lift_lift_comp_vlift,
-      Subst.vsubst_lift_comp_liftn, *]
-
-def lsubst0 (r : Region φ) : Subst φ
-  | 0 => r
-  | ℓ + 1 => br ℓ (Term.var 0)
-
-def alpha (ℓ : ℕ) (r : Region φ) : Subst φ
-  := Function.update Subst.id ℓ r
-
-def Subst.toFCFG (σ : Subst φ) (n : ℕ) : Fin n → Region φ | i => σ i
-
-def Subst.fromFCFG (k : ℕ) (σ : Fin n → Region φ) : Subst φ
-  | i => if h : i < n then σ ⟨i, h⟩ else br (i - n + k) (Term.var 0)
-
-def Subst.extend (σ : Subst φ) (n : ℕ) (k : ℕ) : Subst φ
-  | i => if i < n then σ i else br (i - n + k) (Term.var 0)
-
-@[simp]
-theorem Subst.extend_lt {σ : Subst φ} {n k i} (hi : i < n)
-  : σ.extend n k i = σ i := by simp [extend, *]
-
-@[simp]
-theorem Subst.extend_ge {σ : Subst φ} {n k i} (hi : i ≥ n)
-  : σ.extend n k i = br (i - n + k) (Term.var 0) := by simp [extend, *]
-
-@[simp]
-theorem Subst.fromFCFG_lt {σ : Fin n → Region φ} {i : ℕ} (h : i < n)
-  : Subst.fromFCFG k σ i = σ ⟨i, h⟩ := by simp [Subst.fromFCFG, h]
-
-theorem Subst.fromFCFG_fin {σ : Fin n → Region φ} {i : Fin n}
-  : Subst.fromFCFG k σ i = σ i := by simp
-
-theorem Subst.fromFCFG_zero_zero {σ : Fin 0 → Region φ}
-  : Subst.fromFCFG 0 σ = Subst.id := by funext i; rfl
-
-theorem Subst.fromFCFG_zero_one {σ : Fin 1 → Region φ}
-  : Subst.fromFCFG 0 σ = (σ 0).lsubst0 := by funext i; cases i <;> rfl
-
-theorem Subst.fromFCFG_one_one {σ : Fin 1 → Region φ}
-  : Subst.fromFCFG 1 σ = (σ 0).alpha 0 := by funext i; cases i <;> rfl
-
-theorem Subst.fromFCFG_zero_elim1 {r : Region φ}
-  : Subst.fromFCFG 0 (Fin.elim1 r) = r.lsubst0 := by rw [Subst.fromFCFG_zero_one]; rfl
-
-theorem Subst.fromFCFG_one_elim1 {r : Region φ}
-  : Subst.fromFCFG 1 (Fin.elim1 r) = r.alpha 0 := by rw [Subst.fromFCFG_one_one]; rfl
-
-theorem Subst.toFCFG_fromFCFG (σ : Fin n → Region φ) : Subst.toFCFG (Subst.fromFCFG k σ) n = σ := by
-  funext i
-  cases i
-  simp [fromFCFG, toFCFG, *]
-
-theorem Subst.fromFCFG_toFCFG (σ : Subst φ) (n : ℕ)
-  : Subst.fromFCFG k (Subst.toFCFG σ n) = σ.extend n k
-  := by funext i; simp [fromFCFG, toFCFG, extend]
-
-def Subst.trunc (σ : Subst φ) (n : ℕ) : Subst φ
-  | i => if i < n then σ i else br i (Term.var 0)
-
-@[simp]
-theorem Subst.trunc_trunc {σ : Subst φ} {n m : ℕ}
-  : (σ.trunc n).trunc m = σ.trunc (min n m) := by
-  funext i
-  simp only [trunc, lt_min_iff]
-  split <;> split
-  case isFalse.isTrue h h' => exact (h h'.right).elim
-  all_goals simp [*]
-
-theorem Subst.trunc_trunc_self {σ : Subst φ} {n : ℕ}
-  : (σ.trunc n).trunc n = σ.trunc n := by simp
-
-theorem Subst.trunc_comm {σ : Subst φ} {n m : ℕ}
-  : (σ.trunc n).trunc m = (σ.trunc m).trunc n := by simp [min_comm]
-
-theorem Subst.extend_same {σ : Subst φ} {n : ℕ}
-  : σ.extend n n = σ.trunc n := by
-  funext i
-  simp only [extend, trunc]
-  split
-  case isTrue h => rfl
-  case isFalse h => simp [Nat.ge_of_not_lt h]
-
-theorem Subst.extend_eq_of_eq_on {σ τ : Subst φ} {n k : ℕ} (h : (Set.Iio n).EqOn σ τ)
-  : σ.extend n k = τ.extend n k := by
-  funext i
-  simp only [extend]
-  split
-  case isTrue h' => exact h h'
-  case isFalse h' => simp [Nat.ge_of_not_lt h']
-
-theorem Subst.eq_on_of_extend_eq {σ τ : Subst φ} {n k : ℕ}
-  (h : σ.extend n k = τ.extend n k)
-  : (Set.Iio n).EqOn σ τ := λi hi => by
-  have h := congrFun h i
-  simp only [extend, Set.mem_Iio.mp hi, ↓reduceIte] at h
-  exact h
-
-theorem Subst.extend_eq_iff {σ τ : Subst φ} {n k : ℕ}
-  : σ.extend n k = τ.extend n k ↔ (Set.Iio n).EqOn σ τ := ⟨
-    Subst.eq_on_of_extend_eq,
-    Subst.extend_eq_of_eq_on
-  ⟩
-
-theorem Subst.trunc_eq_iff {σ τ : Subst φ} {n : ℕ}
-  : σ.trunc n = τ.trunc n ↔ (Set.Iio n).EqOn σ τ := by simp only [<-extend_same, extend_eq_iff]
-
-theorem Subst.trunc_eq_of_eq_on {σ τ : Subst φ} {n : ℕ}
-  (h : (Set.Iio n).EqOn σ τ) : σ.trunc n = τ.trunc n := trunc_eq_iff.mpr h
-
-theorem Subst.eq_on_of_trunc_eq {σ τ : Subst φ} {n : ℕ}
-  (h : σ.trunc n = τ.trunc n) : (Set.Iio n).EqOn σ τ := trunc_eq_iff.mp h
-
-def csubst (r : Region φ) : Subst φ := λ_ => r
-
-@[simp]
-theorem Subst.csubst_apply {r : Region φ} {i : ℕ} : r.csubst i = r := rfl
-
-theorem Subst.extend_alphan {r : Region φ}
-  : (r.alpha n).extend (k + n + 1) (k + n + 1) = r.alpha n := by
-  funext i
-  simp [extend, Subst.id, alpha, Function.update]
-  intro h
-  rw [ite_cond_eq_false]
-  simp only [br.injEq, and_true]
-  omega
-  simp only [eq_iff_iff, iff_false]
-  omega
-
-theorem Subst.extend_alpha0 {r : Region φ} : (r.alpha 0).extend (k + 1) (k + 1) = r.alpha 0
-  := by rw [extend_alphan]
-
-end Region
-
-/-- Substitute the free labels in this control-flow graph -/
-def CFG.lsubst (σ : Region.Subst φ) (G : CFG φ) : CFG φ where
-  length := G.length
-  targets := λ i => (G.targets i).lsubst σ
-
-end BinSyntax
+import DeBruijnSSA.BinSyntax.Syntax.Subst.Term
+import DeBruijnSSA.BinSyntax.Syntax.Subst.Terminator
+import DeBruijnSSA.BinSyntax.Syntax.Subst.Region
diff --git a/DeBruijnSSA/BinSyntax/Syntax/Subst/Region.lean b/DeBruijnSSA/BinSyntax/Syntax/Subst/Region.lean
new file mode 100644
index 0000000..83a4c29
--- /dev/null
+++ b/DeBruijnSSA/BinSyntax/Syntax/Subst/Region.lean
@@ -0,0 +1,739 @@
+import Discretion.Wk.Nat
+import Discretion.Wk.Fin
+import Discretion.Wk.Multiset
+import Discretion.Wk.Multiset
+
+import DeBruijnSSA.BinSyntax.Syntax.Subst.Term
+
+namespace BinSyntax
+
+/-! ### Region substitutions
+ -/
+namespace Region
+
+/-- A substitution mapping labels to regions -/
+def Subst (φ : Type _) := ℕ → Region φ -- TODO: Region.Subst?
+
+/-- The identity substitution, which maps labels to themselves -/
+def Subst.id : Subst φ := λn => Region.br n (Term.var 0)
+
+theorem Subst.id_apply (n : ℕ) : @Subst.id φ n = Region.br n (Term.var 0) := rfl
+
+/-- Lift a substitution under a label binder -/
+def Subst.lift (σ : Subst φ) : Subst φ
+  | 0 => Region.br 0 (Term.var 0)
+  | n + 1 => (σ n).lwk Nat.succ
+
+/-- Lift a substitution under `n` label binders -/
+def Subst.liftn (n : ℕ) (σ : Subst φ) : Subst φ
+  := λm => if m < n then Region.br m (Term.var 0) else (σ (m - n)).lwk (λv => v + n)
+
+@[simp]
+theorem Subst.liftn_zero (σ : Subst φ) : σ.liftn 0 = σ := by
+  funext n
+  simp only [liftn]
+  split
+  · rename_i H; cases H
+  · exact (σ n).lwk_id
+
+theorem Subst.liftn_one (σ : Subst φ) : σ.liftn 1 = σ.lift := by funext m; cases m <;> rfl
+
+theorem Subst.liftn_succ (n) (σ: Subst φ) : σ.liftn n.succ = (σ.liftn n).lift := by
+  induction n with
+  | zero => rw [σ.liftn_one, σ.liftn_zero]
+  | succ n I => -- TODO: I'm sure this can be made _much_ cleaner...
+    funext m
+    rw [I]
+    simp only [lift]
+    split
+    · rfl
+    · simp only [liftn]
+      split
+      · split
+        · rfl
+        · split
+          · rfl
+          · rename_i H C; exact (C (Nat.lt_of_succ_lt_succ (Nat.lt_of_succ_lt_succ H))).elim
+      · split
+        · rename_i H; simp_arith at H
+        · split
+          · rename_i C H; exact (C (Nat.succ_lt_succ (Nat.succ_lt_succ H))).elim
+          · simp only [Region.lwk_lwk]
+            apply congr
+            apply congrArg
+            funext v
+            simp_arith
+            simp_arith
+
+theorem Subst.liftn_eq_iterate_lift_apply (n: ℕ) (σ: Subst φ) : σ.liftn n = (Subst.lift^[n] σ) := by
+  induction n with
+  | zero => exact σ.liftn_zero
+  | succ n => simp only [Function.iterate_succ_apply', Subst.liftn_succ, *]
+
+theorem Subst.liftn_eq_iterate_lift (n: ℕ) : Subst.liftn n = (@Subst.lift φ)^[n] := by
+  funext σ
+  rw [liftn_eq_iterate_lift_apply]
+
+theorem Subst.liftn_succ' (n) (σ: Subst φ) : σ.liftn n.succ = σ.lift.liftn n := by
+  simp [liftn_eq_iterate_lift]
+
+@[simp]
+theorem Subst.lift_id : (@id φ).lift = id := by funext n; cases n <;> rfl
+
+@[simp]
+theorem Subst.iterate_lift_id : (n: ℕ) -> Subst.lift^[n] (@id φ) = id
+  | 0 => rfl
+  | n + 1 => by simp [lift_id, iterate_lift_id n]
+
+@[simp]
+theorem Subst.liftn_id (n: ℕ): (@id φ).liftn n = id := by
+  rw [liftn_eq_iterate_lift_apply, iterate_lift_id]
+
+theorem Subst.liftn_add (n m: ℕ) : Subst.liftn (m + n) = (@Subst.liftn α m) ∘ (@Subst.liftn α n)
+  := by simp [liftn_eq_iterate_lift, Function.iterate_add]
+
+theorem Subst.liftn_liftn (n m: ℕ) (σ: Subst φ): (σ.liftn n).liftn m = σ.liftn (m + n)
+  := by simp [liftn_add]
+
+theorem Subst.lift_succ (σ : Subst φ) (i : ℕ) : σ.lift (i + 1) = (σ i).lwk Nat.succ := rfl
+
+/-- Lift a substitution under a variable binder -/
+def Subst.vlift (σ : Subst φ) : Subst φ := vwk1 ∘ σ
+
+@[simp]
+theorem Subst.vlift_id : (@id φ).vlift = id := by funext v; cases v <;> rfl
+
+theorem Subst.vlift_lift_comm (σ : Subst σ) : σ.lift.vlift = σ.vlift.lift := by
+  funext n
+  cases n with
+  | zero => rfl
+  | succ n => simp [Subst.vlift, vwk1, lift, vwk_lwk]
+
+theorem Subst.vlift_lift_comp_comm : Subst.vlift ∘ (@Subst.lift φ) = Subst.lift ∘ Subst.vlift
+  := funext Subst.vlift_lift_comm
+
+theorem Subst.vlift_liftn_comm (n : ℕ) (σ : Subst σ) : (σ.liftn n).vlift = σ.vlift.liftn n := by
+  induction n generalizing σ with
+  | zero => simp
+  | succ _ I => rw [liftn_succ, vlift_lift_comm, I, liftn_succ]
+
+/-- Lift a substitution under `n` variable binders -/
+def Subst.vliftn (n : ℕ) (σ : Subst φ) : Subst φ
+  := Region.vwk (Nat.liftWk (λi => i + n)) ∘ σ
+
+@[simp]
+theorem Subst.vliftn_zero (σ : Subst φ) : σ.vliftn 0 = σ := by
+  funext n
+  simp [vliftn]
+
+theorem Subst.vliftn_one (σ : Subst φ) : σ.vliftn 1 = σ.vlift := by
+  funext n
+  simp [vliftn, vlift, vwk1]
+
+theorem Subst.vliftn_succ (σ : Subst φ) (i : ℕ) : σ.vliftn (i + 1) = (σ.vliftn i).vlift := by
+  funext ℓ
+  simp only [vliftn, vwk1, Function.comp_apply, vlift, vwk_vwk]
+  congr
+  funext n
+  cases n <;> rfl
+
+theorem Subst.vliftn_two (σ : Subst φ) : σ.vliftn 2 = σ.vlift.vlift := by
+  rw [Subst.vliftn_succ, Subst.vliftn_succ]; simp
+
+theorem Subst.vliftn_eq_iterate_vlift_apply (n: ℕ) (σ: Subst φ) : σ.vliftn n = (Subst.vlift^[n] σ)
+  := by induction n with
+  | zero => exact σ.vliftn_zero
+  | succ n => simp only [Function.iterate_succ_apply', Subst.vliftn_succ, *]
+
+theorem Subst.vliftn_eq_iterate_vlift (n: ℕ) : Subst.vliftn n = (@Subst.vlift φ)^[n] := by
+  funext σ
+  rw [vliftn_eq_iterate_vlift_apply]
+
+theorem Subst.vliftn_succ' (σ : Subst φ) (i : ℕ) : σ.vliftn (i + 1) = σ.vlift.vliftn i
+  := by simp [vliftn_eq_iterate_vlift]
+
+theorem Subst.vliftn_add (σ : Subst φ) (n m: ℕ) : σ.vliftn (n + m) = (σ.vliftn m).vliftn n := by
+  funext k
+  simp [vliftn_eq_iterate_vlift, Function.iterate_add_apply]
+
+theorem Subst.iterate_vlift_id : (n: ℕ) -> Subst.vlift^[n] (@id φ) = id
+  | 0 => rfl
+  | n + 1 => by simp [Subst.vlift_id, iterate_vlift_id n]
+
+@[simp]
+theorem Subst.vliftn_id (n: ℕ): (@id φ).vliftn n = id := by
+  rw [vliftn_eq_iterate_vlift_apply, iterate_vlift_id]
+
+theorem Subst.iterate_vlift_liftn_comm (k n : ℕ) (σ: Subst φ)
+  : Subst.vlift^[k] (σ.liftn n) = (Subst.vlift^[k] σ).liftn n := by
+  induction k generalizing σ with
+  | zero => rfl
+  | succ n I => simp [I, vlift_liftn_comm]
+
+theorem Subst.vliftn_liftn (k n : ℕ) (σ: Subst φ)
+  : (σ.liftn n).vliftn k = (σ.vliftn k).liftn n
+  := by simp [vliftn_eq_iterate_vlift, iterate_vlift_liftn_comm]
+
+/-- Substitute the labels in a `Region` using `σ` -/
+@[simp]
+def lsubst (σ : Subst φ) : Region φ → Region φ
+  | br n e => (σ n).vsubst e.subst0
+  | case e s t => case e (lsubst σ.vlift s) (lsubst σ.vlift t)
+  | let1 e t => let1 e (lsubst σ.vlift t)
+  | let2 e t => let2 e (lsubst (σ.vliftn 2) t)
+  | cfg β n f => cfg (lsubst (σ.liftn n) β) n (λ i => lsubst (σ.liftn n).vlift (f i))
+
+theorem lsubst_id_apply (t : Region φ) : t.lsubst Subst.id = t
+  := by induction t <;> simp [*]
+
+@[simp]
+theorem lsubst_id : @lsubst φ (Subst.id) = id := funext lsubst_id_apply
+
+theorem lsubst_id_apply' (t : Region φ) : t.lsubst (λi => Region.br i (Term.var 0)) = t
+  := t.lsubst_id_apply
+
+@[simp]
+theorem lsubst_id' : @lsubst φ (λi => Region.br i (Term.var 0)) = id := funext lsubst_id_apply'
+
+theorem lsubst_id_eq {t : Region φ} {σ : Subst φ} (hσ : σ = Subst.id)
+  : t.lsubst σ = t := by cases hσ; simp
+
+theorem lsubst_cfg
+  : @lsubst φ σ (cfg β n G) = cfg (lsubst (σ.liftn n) β) n (lsubst (σ.liftn n).vlift ∘ G)
+  := rfl
+
+theorem lsubst_cfg1
+  : @lsubst φ σ (cfg β 1 (Fin.elim1 G))
+  = cfg (lsubst σ.lift β) 1 (Fin.elim1 $ lsubst σ.lift.vlift G) := by
+  simp only [lsubst, cfg.injEq, heq_eq_eq, true_and, Subst.liftn_one]
+  funext i; cases i using Fin.elim1; rfl
+
+/-- Create a substitution from a label renaming -/
+def Subst.fromLwk (ρ : ℕ -> ℕ): Subst φ := λn => Region.br (ρ n) (Term.var 0)
+
+@[simp]
+theorem Subst.vwk_lift_comp_fromLwk (ρ σ) : vwk (Nat.liftWk ρ) ∘ fromLwk σ = @fromLwk φ σ := rfl
+
+@[simp]
+theorem Subst.vwk1_comp_fromLwk (σ) : vwk1 ∘ fromLwk σ = @fromLwk φ σ := rfl
+
+@[simp]
+theorem Subst.vwk_lift_comp_id (ρ) : vwk (Nat.liftWk ρ) ∘ Subst.id = @Subst.id φ := rfl
+
+@[simp]
+theorem Subst.vsubst_lift_comp_id (σ : Term.Subst φ) : vsubst σ.lift ∘ Subst.id = Subst.id := rfl
+
+@[simp]
+theorem Subst.fromLwk_vlift (ρ) : (@fromLwk φ ρ).vlift = fromLwk ρ := rfl
+
+@[simp]
+theorem Subst.fromLwk_iterate_vlift (n : ℕ) (ρ)
+  : Subst.vlift^[n] (@fromLwk φ ρ) = fromLwk ρ
+  := by induction n <;> simp [fromLwk_vlift, *]
+
+@[simp]
+theorem Subst.fromLwk_vliftn (n ρ) : (@fromLwk φ ρ).vliftn n = fromLwk ρ := by
+  rw [vliftn_eq_iterate_vlift, fromLwk_iterate_vlift]
+
+@[simp]
+theorem Subst.fromLwk_apply (ρ : ℕ -> ℕ) (n : ℕ)
+  : (@fromLwk φ ρ) n = Region.br (ρ n) (Term.var 0) := rfl
+
+theorem Subst.fromLwk_lift (ρ) : (@fromLwk φ ρ).lift = fromLwk (Nat.liftWk ρ) := by
+  funext n; cases n <;> rfl
+
+theorem Subst.fromLwk_iterate_lift (n : ℕ) (ρ)
+  : Subst.lift^[n] (@fromLwk φ ρ) = fromLwk (Nat.liftWk^[n] ρ)
+  := by induction n generalizing ρ <;> simp [fromLwk_lift, *]
+
+theorem Subst.fromLwk_liftn (n ρ) : (@fromLwk φ ρ).liftn n = fromLwk (Nat.liftnWk n ρ) := by
+  rw [liftn_eq_iterate_lift, Nat.liftnWk_eq_iterate_liftWk, fromLwk_iterate_lift]
+
+theorem lsubst_fromLwk_apply (ρ : ℕ -> ℕ) (t : Region φ)
+  : t.lsubst (Subst.fromLwk ρ) = t.lwk ρ := by
+  induction t generalizing ρ
+  <;> simp [Region.lsubst, Region.lwk, Term.subst_fromWk_apply, Subst.fromLwk_liftn, *]
+
+theorem lsubst_fromLwk (ρ : ℕ -> ℕ) : lsubst (Subst.fromLwk ρ) = @lwk φ ρ
+  := funext (lsubst_fromLwk_apply ρ)
+
+theorem lsubst_comp_fromLwk : @lsubst φ ∘ (@Subst.fromLwk φ) = lwk := funext lsubst_fromLwk
+
+theorem lsubst_liftn (n : ℕ) (σ : Subst φ) (t : Region φ)
+    : (t.lwk (Nat.liftnWk n Nat.succ)).lsubst (σ.liftn (n + 1))
+      = (t.lsubst (σ.liftn n)).lwk (Nat.liftnWk n Nat.succ)
+  := by induction t generalizing σ n with
+  | br ℓ e =>
+    simp only [lwk, lsubst, Nat.liftnWk, Subst.liftn]
+    split
+    · split
+      · simp [lwk, Nat.liftnWk, *]
+      · rename_i H C; exact (C (Nat.le_step H)).elim
+    · rename_i C
+      simp_arith only [ite_false]
+      rw [Nat.succ_eq_add_one]
+      have h : ℓ - n + 1 + n - (n + 1) = ℓ - n := by
+        rw [Nat.add_assoc, Nat.add_comm 1 n, Nat.add_sub_cancel]
+      rw [h, Region.lwk_vsubst, lwk_lwk]
+      congr
+      funext n
+      simp_arith [Nat.liftnWk]
+  | cfg β k G Iβ IG => simp only [
+    Subst.vlift_liftn_comm, lsubst, lwk, Subst.liftn_liftn,
+    <-Nat.add_assoc, <-Nat.liftnWk_add_apply, *]
+  | _ => simp [Subst.vlift_liftn_comm, Subst.vliftn_liftn, *]
+
+theorem lsubst_iterate_lift (n : ℕ) (σ : Subst φ) (t : Region φ)
+  : (t.lwk (Nat.liftWk^[n] Nat.succ)).lsubst (Subst.lift^[n + 1] σ)
+    = (t.lsubst (Subst.lift^[n] σ)).lwk (Nat.liftWk^[n] Nat.succ)
+  := by simp only [<-Subst.liftn_eq_iterate_lift, <-Nat.liftnWk_eq_iterate_liftWk, lsubst_liftn]
+
+theorem lsubst_lift (t : Region φ) (σ : Subst φ)
+  : (t.lwk Nat.succ).lsubst (σ.lift) = (t.lsubst σ).lwk Nat.succ := t.lsubst_iterate_lift 0 σ
+
+/-- Compose two label-substitutions to yield another -/
+def Subst.comp (σ τ : Subst φ): Subst φ
+  | n => (τ n).lsubst σ.vlift
+
+@[simp]
+theorem Subst.comp_id (σ : Subst φ) : σ.comp Subst.id = σ := by
+  funext n
+  simp only [comp, Region.lsubst, Function.comp_apply, vlift, vwk1]
+  rw [<-Region.vsubst_fromWk_apply, <-Region.vsubst_comp_apply]
+  simp
+
+@[simp]
+theorem Subst.id_comp (σ : Subst φ) : Subst.id.comp σ = σ
+  := by funext n; exact lsubst_id_apply (σ n)
+
+theorem Subst.vlift_comp_liftWk_stepn (σ : Subst φ) (n)
+    : vlift (vwk (Nat.liftWk (· + n)) ∘ σ) = vwk (Nat.liftWk (· + n)) ∘ σ.vlift := by
+  simp only [vlift, vwk1, <-Function.comp.assoc]
+  apply congrArg₂
+  funext i
+  simp only [Function.comp_apply, vwk_vwk]
+  apply congrArg₂
+  funext i
+  simp only [Function.comp_apply, Nat.wkn]
+  cases i <;> simp_arith
+  rfl
+  rfl
+
+theorem Subst.vlift_comp_liftWk_succ (σ : Subst φ)
+  : vlift (vwk (Nat.liftWk Nat.succ) ∘ σ) = vwk (Nat.liftWk Nat.succ) ∘ σ.vlift
+  := rfl
+
+theorem Subst.vlift_comp_wk1 (σ : Subst φ)
+  : vlift (vwk (Nat.wkn 1) ∘ σ) = vwk (Nat.wkn 1) ∘ σ.vlift
+  := Nat.wkn_one ▸ vlift_comp_liftWk_succ σ
+
+theorem vsubst_substn_lsubst_vliftn (t : Region φ) (e : Term φ) (σ : Subst φ) (n)
+  : (t.lsubst (σ.vliftn (n + 1))).vsubst (e.substn n)
+  = (t.vsubst (e.substn n)).lsubst (σ.vliftn n)
+  := by induction t generalizing σ e n with
+  | br ℓ e' =>
+    simp only [
+      lsubst, Subst.vliftn, <-Region.vsubst_fromWk, <-Region.vsubst_comp_apply,
+      Function.comp_apply]
+    congr
+    funext k
+    cases k with
+    | zero => rfl
+    | succ k => simp_arith [Term.Subst.comp, Term.subst, Term.substn, Nat.liftWk]
+  | _ => simp only [
+    vsubst, lsubst,  <-Subst.vliftn_succ, <-Term.substn_succ,
+    <-Subst.vliftn_add, <-Nat.add_assoc, <-Term.substn_add_right,
+    <-Subst.vliftn_liftn, *
+  ]
+
+theorem vsubst_subst0_lsubst_vlift (t : Region φ) (e : Term φ) (σ : Subst φ)
+    : (t.lsubst σ.vlift).vsubst e.subst0 = (t.vsubst e.subst0).lsubst σ := by
+  have h := vsubst_substn_lsubst_vliftn t e σ 0
+  simp only [Term.substn_zero, Subst.vliftn_zero, Subst.vliftn_one, Nat.zero_add] at h
+  exact h
+
+theorem vsubst_substn_vwk (t : Region φ) (e : Term φ) (ρ n)
+  : (t.vsubst (e.substn n)).vwk (Nat.liftnWk n ρ)
+  = (t.vwk (Nat.liftnWk (n + 1) ρ)).vsubst ((e.wk (Nat.liftnWk n ρ)).substn n)
+  := by induction t generalizing e ρ n <;> simp [
+        <-Nat.liftnWk_succ_apply', ← Nat.liftnWk_add_apply,
+        <-Term.substn_succ, Term.subst_substn_wk,
+        Term.wk_wk, Nat.liftnWk_comp_succ,  ← Term.substn_add_right,
+        <-Nat.add_assoc, Nat.liftnWk_comp_add_right, *
+      ]
+
+theorem vsubst_subst0_vwk (t : Region φ) (e : Term φ) (ρ)
+  : (t.vsubst e.subst0).vwk ρ = (t.vwk (Nat.liftWk ρ)).vsubst (e.wk ρ).subst0 := by
+  have h := vsubst_substn_vwk t e ρ 0
+  simp [Nat.liftnWk_one, Nat.liftnWk_zero, Term.substn_zero] at h
+  exact h
+
+theorem Subst.vwk_liftWk_comp_liftn (σ : Subst φ) (ρ)
+    : vwk (Nat.liftWk ρ) ∘ σ.liftn n = liftn n (vwk (Nat.liftWk ρ) ∘ σ) := by
+  funext k
+  simp only [Function.comp_apply, liftn]
+  split
+  rfl
+  rw [lwk_vwk]
+
+theorem Subst.vwk_liftWk_liftWk_comp_vlift (σ : Subst φ) (ρ)
+    : vwk (Nat.liftWk (Nat.liftWk ρ)) ∘ σ.vlift = vlift (vwk (Nat.liftWk ρ) ∘ σ) := by
+  simp only [vlift, vwk1, ← Function.comp.assoc, ← vwk_comp, ← Nat.liftWk_comp, Nat.liftWk_comp_succ]
+
+theorem Subst.vwk_liftWk_liftnWk_comp_vliftn (n : ℕ) (σ : Subst φ) (ρ)
+    : vwk (Nat.liftWk (Nat.liftnWk n ρ)) ∘ σ.vliftn n = vliftn n (vwk (Nat.liftWk ρ) ∘ σ) := by
+  simp only [vliftn, ← Function.comp.assoc, ← vwk_comp, ← Nat.liftWk_comp, Nat.liftnWk_comp_add]
+
+theorem vwk_lsubst (σ ρ) (t : Region φ)
+  : (t.lsubst σ).vwk ρ = (t.vwk ρ).lsubst (vwk (Nat.liftWk ρ) ∘ σ)
+  := by induction t generalizing σ ρ with
+  | br ℓ e => simp [vsubst_subst0_vwk]
+  | _ =>
+    simp only [
+      vwk, lsubst,
+      Subst.vwk_liftWk_liftWk_comp_vlift, Subst.vwk_liftWk_liftnWk_comp_vliftn,
+      Subst.vwk_liftWk_comp_liftn, *]
+
+theorem vwk1_lsubst (σ) (t : Region φ)
+  : (t.lsubst σ).vwk1 = t.vwk1.lsubst (vwk2 ∘ σ)
+  := by rw [vwk1, vwk_lsubst, vwk2, Nat.liftnWk_two]; rfl
+
+theorem Subst.vliftn_comp (n : ℕ) (σ τ : Subst φ)
+  : (σ.comp τ).vliftn n = (σ.vliftn n).comp (τ.vliftn n)
+  := by
+  funext m
+  simp only [Function.comp_apply, comp, vlift, vliftn, vwk1, Function.comp_apply]
+  generalize τ m = t
+  rw [vwk_lsubst]
+  simp only [<-Function.comp.assoc, <-vwk_comp, <-Nat.liftWk_comp, Nat.liftWk_comp_succ]
+
+theorem Subst.vlift_comp (σ τ : Subst φ) : (σ.comp τ).vlift = σ.vlift.comp τ.vlift
+  := σ.vliftn_comp 1 τ
+
+theorem Subst.lwk_comp_vlift (ρ) (σ : Subst φ) : lwk ρ ∘ σ.vlift = vlift (lwk ρ ∘ σ)
+  := by simp only [vlift, vwk1, <-Function.comp.assoc, vwk_comp_lwk]
+
+theorem Subst.lwk_comp_vliftn (ρ) (σ : Subst φ) (n) : lwk ρ ∘ σ.vliftn n = vliftn n (lwk ρ ∘ σ)
+  := by simp only [vliftn, <-Function.comp.assoc, vwk_comp_lwk]
+
+theorem Subst.vlift_comp_lwk (σ : Subst φ) (ρ) : vlift (σ ∘ ρ) = σ.vlift ∘ ρ := rfl
+
+theorem Subst.vliftn_comp_lwk (σ : Subst φ) (ρ) (n) : vliftn n (σ ∘ ρ) = σ.vliftn n ∘ ρ := rfl
+
+theorem Subst.liftn_comp_lwk (σ : Subst φ) (ρ) (n) : liftn n (σ ∘ ρ) = σ.liftn n ∘ Nat.liftnWk n ρ
+  := by funext i; simp only [liftn, Function.comp_apply, Nat.liftnWk]; split <;> simp_arith
+
+theorem Subst.liftn_lwk_comp (σ : Subst φ) (ρ) (n)
+    : liftn n (lwk ρ ∘ σ) = lwk (Nat.liftnWk n ρ) ∘ σ.liftn n := by
+  funext i
+  simp only [liftn, Function.comp_apply, lwk, Nat.liftnWk]
+  split
+  · simp [Nat.liftnWk, *]
+  · rw [lwk_lwk, lwk_lwk, Nat.liftnWk_comp_add]
+
+theorem lwk_lsubst (σ ρ) (t : Region φ)
+  : (t.lsubst σ).lwk ρ = t.lsubst (lwk ρ ∘ σ)
+  := by induction t generalizing σ ρ with
+  | br ℓ e => simp only [lsubst, Function.comp_apply, lwk_vsubst]
+  | _ => simp [Subst.lwk_comp_vlift, Subst.lwk_comp_vliftn, Subst.liftn_lwk_comp , *]
+
+theorem lsubst_lwk (σ ρ) (t : Region φ)
+  : (t.lwk ρ).lsubst σ = t.lsubst (σ ∘ ρ) := by
+  induction t generalizing σ ρ with
+  | br ℓ e => rfl
+  | _ => simp [Subst.vlift_comp_lwk, Subst.vliftn_comp_lwk, Subst.liftn_comp_lwk, *]
+
+theorem Subst.liftn_comp_add (n) (σ : Subst φ) : σ.liftn n ∘ (· + n) = lwk (· + n) ∘ σ := by
+  funext i; simp [liftn]
+
+theorem Subst.liftn_comp (n : ℕ) (σ τ : Subst φ) : (σ.comp τ).liftn n = (σ.liftn n).comp (τ.liftn n)
+  := by
+  funext k
+  simp only [liftn, comp]
+  split
+  case isTrue h => simp [liftn, vlift, h]
+  case isFalse h =>
+    rw [lwk_lsubst, lsubst_lwk]
+    congr
+    rw [lwk_comp_vlift, vlift, vlift, Function.comp.assoc, liftn_comp_add]
+
+theorem Subst.lift_comp (σ τ : Subst φ) : (σ.comp τ).lift = σ.lift.comp τ.lift := by
+  have h := Subst.liftn_comp 1 σ τ
+  simp only [Subst.liftn_one] at h
+  exact h
+
+theorem lsubst_lsubst (σ τ : Subst φ) (t : Region φ)
+  : (t.lsubst τ).lsubst σ = t.lsubst (σ.comp τ)
+  := by induction t generalizing σ τ with
+  | br ℓ e => simp only [lsubst, Subst.comp, vsubst_subst0_lsubst_vlift]
+  | _ => simp only [lsubst, Subst.comp, Subst.vlift_comp, Subst.vliftn_comp, Subst.liftn_comp, *]
+
+theorem lsubst_comp (σ τ : Subst φ)
+  : Region.lsubst (σ.comp τ) = Region.lsubst σ ∘ Region.lsubst τ
+  := Eq.symm $ funext $ lsubst_lsubst σ τ
+
+/-- Substitute the labels in a `Region` using `σ` and let-bindings -/
+@[simp]
+def llsubst (σ : Subst φ) : Region φ → Region φ
+  := lsubst (let1 (Term.var 0) ∘ σ.vlift)
+
+/-- Compose two label-substitutions via let-bindings to yield another -/
+def Subst.lcomp (σ τ : Subst φ): Subst φ
+  | n => (τ n).llsubst σ.vlift
+
+theorem Subst.vlift_let1_zero (σ : Subst φ)
+    : vlift (let1 (Term.var 0) ∘ σ.vlift) = let1 (Term.var 0) ∘ σ.vlift.vlift :=
+  by funext k; simp [vlift, vwk1, vwk_vwk, <-Nat.liftWk_comp, Nat.liftWk_comp_succ]
+
+theorem Subst.vliftn_let1_zero (σ : Subst φ)
+    : vliftn n (let1 (Term.var 0) ∘ σ.vlift) = let1 (Term.var 0) ∘ (σ.vliftn n).vlift :=
+  by induction n with
+  | zero => simp
+  | succ n I => rw [vliftn_succ, I, vlift_let1_zero, vliftn_succ]
+
+theorem llsubst_lcomp (σ τ : Subst φ) : llsubst (σ.lcomp τ) = llsubst σ ∘ llsubst τ := by
+  simp only [llsubst, <-lsubst_comp]
+  apply congrArg
+  funext k
+  simp only [Subst.vlift, vwk1, Function.comp_apply, Subst.lcomp, llsubst, Subst.comp, lsubst, let1.injEq,
+    true_and]
+  rw [vwk_lsubst]
+  congr
+  funext k
+  simp only [Function.comp_apply, vwk, Term.wk, Nat.liftWk_zero, let1.injEq, true_and, vwk_vwk]
+  congr
+  simp only [<-Nat.liftWk_comp, Nat.liftWk_comp_succ, <-Function.comp.assoc]
+  rw [Function.comp.assoc, Nat.liftWk_comp_succ, Function.comp.assoc]
+
+theorem llsubst_llsubst (σ τ : Subst φ) (t : Region φ)
+  : (t.llsubst τ).llsubst σ = t.llsubst (σ.lcomp τ)
+  := by rw [llsubst_lcomp]; simp
+
+def let1V0 (r : Region φ) : Region φ := (r.vwk (Nat.liftWk Nat.succ)).let1 (Term.var 0)
+
+theorem lsubst_let1V0_comp (σ : Subst φ) (r : Region φ)
+  : (r.lsubst (let1V0 ∘ σ)) = r.llsubst σ
+  := rfl
+
+def let1Br : Subst φ := λℓ => (br ℓ (Term.var 0)).let1 (Term.var 0)
+
+theorem Subst.let1V0_comp_id : @let1V0 φ ∘ id = let1Br := rfl
+
+theorem lwk_lsubst_swap (σ σ' : Subst φ) (ρ ρ') (r : Region φ)
+  (h : lwk ρ ∘ σ = σ' ∘ ρ')
+  : (r.lsubst σ).lwk ρ = (r.lwk ρ').lsubst σ'
+  := by rw [lwk_lsubst, lsubst_lwk, h]
+
+theorem lsubst_lwk_swap (σ σ' : Subst φ) (ρ ρ') (r : Region φ)
+  (h : σ ∘ ρ = lwk ρ' ∘ σ')
+  : (r.lwk ρ).lsubst σ = (r.lsubst σ').lwk ρ'
+  := by rw [lwk_lsubst, lsubst_lwk, h]
+
+theorem lwk_lsubst_comm (σ : Subst φ) (ρ) (r : Region φ)
+  (h : lwk ρ ∘ σ = σ ∘ ρ)
+  : (r.lsubst σ).lwk ρ = (r.lwk ρ).lsubst σ
+  := lwk_lsubst_swap σ σ ρ ρ r h
+
+theorem lsubst_lwk_comm (σ : Subst φ) (ρ) (r : Region φ)
+  (h : σ ∘ ρ = lwk ρ ∘ σ)
+  : (r.lwk ρ).lsubst σ = (r.lsubst σ).lwk ρ
+  := lsubst_lwk_swap σ σ ρ ρ r h
+
+theorem Subst.liftn_comp_toNatWk {ρ : Fin k → Fin n}
+  : (@liftn φ n σ) ∘ (Fin.toNatWk ρ) = (lwk $ Fin.toNatWk ρ) ∘ (@liftn φ k σ) := by
+  funext i
+  simp only [Function.comp_apply, liftn, Fin.toNatWk]
+  split
+  case isTrue h => simp [Fin.toNatWk, h]
+  case isFalse h =>
+    simp [Nat.sub_add_cancel (Nat.le_of_not_lt h), h, lwk_lwk, Fin.toNatWk_comp_add]
+
+theorem lsubst_liftn_lwk_toNatWk {ρ : Fin k → Fin n}
+    : (lsubst (@Subst.liftn φ n σ) (lwk (Fin.toNatWk ρ) r))
+      = (lwk (Fin.toNatWk ρ) (lsubst (Subst.liftn k σ) r)) := by
+  apply lsubst_lwk_swap
+  apply Subst.liftn_comp_toNatWk
+
+theorem lsubst_liftn_comp_lwk_toNatWk {ρ : Fin k → Fin n}
+    : (lsubst (Subst.liftn n σ) ∘ lwk (Fin.toNatWk ρ))
+      = (lwk (Fin.toNatWk ρ) ∘ lsubst (Subst.liftn k σ)) := by
+  funext r
+  apply lsubst_liftn_lwk_toNatWk
+
+theorem vsubst_lift_lift_comp_vwk1 {ρ : Term.Subst φ}
+  : (vsubst ρ.lift.lift ∘ vwk1) = (vwk1 ∘ vsubst ρ.lift) := by
+  simp only [vwk1, <-vsubst_fromWk, vsubst_comp]
+  apply congrArg
+  funext k
+  cases k with
+  | zero => rfl
+  | succ =>
+    simp only [Term.Subst.comp, Term.subst, Nat.liftWk_succ, Nat.succ_eq_add_one,
+      Term.Subst.lift_succ, Term.wk_wk, Term.subst_fromWk, Nat.liftWk_succ_comp_succ]
+    rfl
+
+theorem vsubst_lift₂_vwk1 {ρ : Term.Subst φ} {r : Region φ}
+  : r.vwk1.vsubst ρ.lift.lift = (r.vsubst ρ.lift).vwk1 := congrFun vsubst_lift_lift_comp_vwk1 r
+
+theorem vsubst_lift_lift_comp_vlift {ρ : Term.Subst φ} {σ : Subst φ}
+  : (vsubst ρ.lift.lift ∘ σ.vlift) = Subst.vlift (vsubst ρ.lift ∘ σ) := by
+  rw [Subst.vlift, <-Function.comp.assoc, vsubst_lift_lift_comp_vwk1]; rfl
+
+theorem Subst.vsubst_lift_comp_liftn (σ : Subst φ) (ρ : Term.Subst φ)
+    : vsubst ρ.lift ∘ σ.liftn n = liftn n (vsubst ρ.lift ∘ σ) := by
+  funext k
+  simp only [Function.comp_apply, liftn]
+  split
+  rfl
+  rw [vsubst_lwk]
+
+theorem vsubst_lsubst (σ ρ) (t : Region φ)
+  : (t.lsubst σ).vsubst ρ = (t.vsubst ρ).lsubst (vsubst ρ.lift ∘ σ)
+  := by induction t generalizing σ ρ with
+  | br ℓ e =>
+    simp only [lsubst, vsubst_vsubst, Function.comp_apply]
+    congr
+    funext k
+    cases k <;> simp [Term.Subst.comp]
+  | _ =>
+    simp only [
+      vsubst, lsubst, Term.Subst.liftn_two, Subst.vliftn_two, vsubst_lift_lift_comp_vlift,
+      Subst.vsubst_lift_comp_liftn, *]
+
+def lsubst0 (r : Region φ) : Subst φ
+  | 0 => r
+  | ℓ + 1 => br ℓ (Term.var 0)
+
+def alpha (ℓ : ℕ) (r : Region φ) : Subst φ
+  := Function.update Subst.id ℓ r
+
+def Subst.toFCFG (σ : Subst φ) (n : ℕ) : Fin n → Region φ | i => σ i
+
+def Subst.fromFCFG (k : ℕ) (σ : Fin n → Region φ) : Subst φ
+  | i => if h : i < n then σ ⟨i, h⟩ else br (i - n + k) (Term.var 0)
+
+def Subst.extend (σ : Subst φ) (n : ℕ) (k : ℕ) : Subst φ
+  | i => if i < n then σ i else br (i - n + k) (Term.var 0)
+
+@[simp]
+theorem Subst.extend_lt {σ : Subst φ} {n k i} (hi : i < n)
+  : σ.extend n k i = σ i := by simp [extend, *]
+
+@[simp]
+theorem Subst.extend_ge {σ : Subst φ} {n k i} (hi : i ≥ n)
+  : σ.extend n k i = br (i - n + k) (Term.var 0) := by simp [extend, *]
+
+@[simp]
+theorem Subst.fromFCFG_lt {σ : Fin n → Region φ} {i : ℕ} (h : i < n)
+  : Subst.fromFCFG k σ i = σ ⟨i, h⟩ := by simp [Subst.fromFCFG, h]
+
+theorem Subst.fromFCFG_fin {σ : Fin n → Region φ} {i : Fin n}
+  : Subst.fromFCFG k σ i = σ i := by simp
+
+theorem Subst.fromFCFG_zero_zero {σ : Fin 0 → Region φ}
+  : Subst.fromFCFG 0 σ = Subst.id := by funext i; rfl
+
+theorem Subst.fromFCFG_zero_one {σ : Fin 1 → Region φ}
+  : Subst.fromFCFG 0 σ = (σ 0).lsubst0 := by funext i; cases i <;> rfl
+
+theorem Subst.fromFCFG_one_one {σ : Fin 1 → Region φ}
+  : Subst.fromFCFG 1 σ = (σ 0).alpha 0 := by funext i; cases i <;> rfl
+
+theorem Subst.fromFCFG_zero_elim1 {r : Region φ}
+  : Subst.fromFCFG 0 (Fin.elim1 r) = r.lsubst0 := by rw [Subst.fromFCFG_zero_one]; rfl
+
+theorem Subst.fromFCFG_one_elim1 {r : Region φ}
+  : Subst.fromFCFG 1 (Fin.elim1 r) = r.alpha 0 := by rw [Subst.fromFCFG_one_one]; rfl
+
+theorem Subst.toFCFG_fromFCFG (σ : Fin n → Region φ) : Subst.toFCFG (Subst.fromFCFG k σ) n = σ := by
+  funext i
+  cases i
+  simp [fromFCFG, toFCFG, *]
+
+theorem Subst.fromFCFG_toFCFG (σ : Subst φ) (n : ℕ)
+  : Subst.fromFCFG k (Subst.toFCFG σ n) = σ.extend n k
+  := by funext i; simp [fromFCFG, toFCFG, extend]
+
+def Subst.trunc (σ : Subst φ) (n : ℕ) : Subst φ
+  | i => if i < n then σ i else br i (Term.var 0)
+
+@[simp]
+theorem Subst.trunc_trunc {σ : Subst φ} {n m : ℕ}
+  : (σ.trunc n).trunc m = σ.trunc (min n m) := by
+  funext i
+  simp only [trunc, lt_min_iff]
+  split <;> split
+  case isFalse.isTrue h h' => exact (h h'.right).elim
+  all_goals simp [*]
+
+theorem Subst.trunc_trunc_self {σ : Subst φ} {n : ℕ}
+  : (σ.trunc n).trunc n = σ.trunc n := by simp
+
+theorem Subst.trunc_comm {σ : Subst φ} {n m : ℕ}
+  : (σ.trunc n).trunc m = (σ.trunc m).trunc n := by simp [min_comm]
+
+theorem Subst.extend_same {σ : Subst φ} {n : ℕ}
+  : σ.extend n n = σ.trunc n := by
+  funext i
+  simp only [extend, trunc]
+  split
+  case isTrue h => rfl
+  case isFalse h => simp [Nat.ge_of_not_lt h]
+
+theorem Subst.extend_eq_of_eq_on {σ τ : Subst φ} {n k : ℕ} (h : (Set.Iio n).EqOn σ τ)
+  : σ.extend n k = τ.extend n k := by
+  funext i
+  simp only [extend]
+  split
+  case isTrue h' => exact h h'
+  case isFalse h' => simp [Nat.ge_of_not_lt h']
+
+theorem Subst.eq_on_of_extend_eq {σ τ : Subst φ} {n k : ℕ}
+  (h : σ.extend n k = τ.extend n k)
+  : (Set.Iio n).EqOn σ τ := λi hi => by
+  have h := congrFun h i
+  simp only [extend, Set.mem_Iio.mp hi, ↓reduceIte] at h
+  exact h
+
+theorem Subst.extend_eq_iff {σ τ : Subst φ} {n k : ℕ}
+  : σ.extend n k = τ.extend n k ↔ (Set.Iio n).EqOn σ τ := ⟨
+    Subst.eq_on_of_extend_eq,
+    Subst.extend_eq_of_eq_on
+  ⟩
+
+theorem Subst.trunc_eq_iff {σ τ : Subst φ} {n : ℕ}
+  : σ.trunc n = τ.trunc n ↔ (Set.Iio n).EqOn σ τ := by simp only [<-extend_same, extend_eq_iff]
+
+theorem Subst.trunc_eq_of_eq_on {σ τ : Subst φ} {n : ℕ}
+  (h : (Set.Iio n).EqOn σ τ) : σ.trunc n = τ.trunc n := trunc_eq_iff.mpr h
+
+theorem Subst.eq_on_of_trunc_eq {σ τ : Subst φ} {n : ℕ}
+  (h : σ.trunc n = τ.trunc n) : (Set.Iio n).EqOn σ τ := trunc_eq_iff.mp h
+
+def csubst (r : Region φ) : Subst φ := λ_ => r
+
+@[simp]
+theorem Subst.csubst_apply {r : Region φ} {i : ℕ} : r.csubst i = r := rfl
+
+theorem Subst.extend_alphan {r : Region φ}
+  : (r.alpha n).extend (k + n + 1) (k + n + 1) = r.alpha n := by
+  funext i
+  simp [extend, Subst.id, alpha, Function.update]
+  intro h
+  rw [ite_cond_eq_false]
+  simp only [br.injEq, and_true]
+  omega
+  simp only [eq_iff_iff, iff_false]
+  omega
+
+theorem Subst.extend_alpha0 {r : Region φ} : (r.alpha 0).extend (k + 1) (k + 1) = r.alpha 0
+  := by rw [extend_alphan]
+
+end Region
+
+/-- Substitute the free labels in this control-flow graph -/
+def CFG.lsubst (σ : Region.Subst φ) (G : CFG φ) : CFG φ where
+  length := G.length
+  targets := λ i => (G.targets i).lsubst σ
+
+end BinSyntax
diff --git a/DeBruijnSSA/BinSyntax/Syntax/Subst/Term.lean b/DeBruijnSSA/BinSyntax/Syntax/Subst/Term.lean
new file mode 100644
index 0000000..c6e7556
--- /dev/null
+++ b/DeBruijnSSA/BinSyntax/Syntax/Subst/Term.lean
@@ -0,0 +1,696 @@
+import Discretion.Wk.Nat
+import Discretion.Wk.Fin
+import Discretion.Wk.Multiset
+import Discretion.Wk.Multiset
+
+import DeBruijnSSA.BinSyntax.Syntax.Definitions
+
+namespace BinSyntax
+
+/-! ### Term substitutions
+ -/
+namespace Term
+
+/-- A substitution mapping variables to terms -/
+def Subst (φ : Type _) := ℕ → Term φ -- TODO: Term.Subst?
+
+/-- The identity substitution, which simply maps variables to themselves -/
+def Subst.id : Subst φ := Term.var
+
+@[simp]
+theorem Subst.id_apply (n : ℕ) : @Subst.id φ n = Term.var n := rfl
+
+/-- Lift a substitution under a binder -/
+def Subst.lift (σ : Subst φ) : Subst φ
+  | 0 => Term.var 0
+  | n + 1 => (σ n).wk Nat.succ
+
+@[simp]
+theorem Subst.lift_zero (σ : Subst φ) : σ.lift 0 = Term.var 0 := rfl
+
+@[simp]
+theorem Subst.lift_succ (σ : Subst φ) (i : ℕ) : σ.lift (i + 1) = (σ i).wk Nat.succ := rfl
+
+/-- Lift a substitution under `n` binders -/
+def Subst.liftn (n : ℕ) (σ : Subst φ) : Subst φ
+  := λm => if m < n then Term.var m else (σ (m - n)).wk (λv => v + n)
+
+@[simp]
+theorem Subst.liftn_zero (σ : Subst φ) : σ.liftn 0 = σ := by
+  funext n
+  simp only [liftn]
+  split
+  · rename_i H; cases H
+  · exact (σ n).wk_id
+
+theorem Subst.liftn_one (σ : Subst φ) : σ.liftn 1 = σ.lift := by funext m; cases m <;> rfl
+
+theorem Subst.liftn_succ (n) (σ: Subst φ) : σ.liftn n.succ = (σ.liftn n).lift := by
+  induction n with
+  | zero => rw [σ.liftn_one, σ.liftn_zero]
+  | succ n I => -- TODO: I'm sure this can be made _much_ cleaner...
+    funext m
+    rw [I]
+    simp only [lift]
+    split
+    · rfl
+    · simp only [liftn]
+      split
+      · split
+        · rfl
+        · split
+          · rfl
+          · rename_i H C; exact (C (Nat.lt_of_succ_lt_succ (Nat.lt_of_succ_lt_succ H))).elim
+      · split
+        · rename_i H; simp_arith at H
+        · split
+          · rename_i C H; exact (C (Nat.succ_lt_succ (Nat.succ_lt_succ H))).elim
+          · simp only [Term.wk_wk]
+            apply congr
+            apply congrArg
+            funext v
+            simp_arith
+            simp_arith
+
+theorem Subst.liftn_two (σ: Subst φ) : σ.liftn 2 = σ.lift.lift
+  := by rw [Subst.liftn_succ, Subst.liftn_one]
+
+theorem Subst.liftn_eq_iterate_lift_apply (n: ℕ) (σ: Subst φ) : σ.liftn n = (Subst.lift^[n] σ) := by
+  induction n with
+  | zero => exact σ.liftn_zero
+  | succ n I => simp only [Function.iterate_succ_apply', Subst.liftn_succ, *]
+
+theorem Subst.liftn_eq_iterate_lift (n: ℕ) : Subst.liftn n = (@Subst.lift φ)^[n] := by
+  funext σ
+  rw [liftn_eq_iterate_lift_apply]
+
+theorem Subst.liftn_succ' (n) (σ: Subst φ) : σ.liftn n.succ = σ.lift.liftn n := by
+  simp [liftn_eq_iterate_lift]
+
+@[simp]
+theorem Subst.lift_id : (@id φ).lift = id := by funext n; cases n <;> rfl
+
+@[simp]
+theorem Subst.iterate_lift_id : (n: ℕ) -> Subst.lift^[n] (@id φ) = id
+  | 0 => rfl
+  | n + 1 => by simp [lift_id, iterate_lift_id n]
+
+@[simp]
+theorem Subst.liftn_id (n: ℕ): (@id φ).liftn n = id := by
+  rw [liftn_eq_iterate_lift_apply, iterate_lift_id]
+
+theorem Subst.liftn_add (n m: ℕ) : Subst.liftn (m + n) = (@Subst.liftn α m) ∘ (@Subst.liftn α n)
+  := by simp [liftn_eq_iterate_lift, Function.iterate_add]
+
+theorem Subst.liftn_liftn (n m: ℕ) (σ: Subst φ): (σ.liftn n).liftn m = σ.liftn (m + n)
+  := by simp [liftn_add]
+
+theorem Subst.liftn_liftn' (n m: ℕ) (σ: Subst φ): (σ.liftn n).liftn m = σ.liftn (n + m)
+  := by simp [liftn_liftn, Nat.add_comm]
+
+/-- Substitute the free variables in a `Term` using `σ` -/
+@[simp]
+def subst (σ : Subst φ) : Term φ → Term φ
+| var x => σ x
+| op f x => op f (subst σ x)
+| let1 a e => let1 (subst σ a) (subst σ.lift e)
+| pair x y => pair (subst σ x) (subst σ y)
+| unit => unit
+| let2 a e => let2 (subst σ a) (subst (σ.liftn 2) e)
+| inl a => inl (subst σ a)
+| inr a => inr (subst σ a)
+| case a l r => case (subst σ a) (subst σ.lift l) (subst σ.lift r)
+| abort a => abort (subst σ a)
+
+@[simp]
+theorem subst_id (t : Term φ) : t.subst Subst.id = t := by induction t <;> simp [*]
+
+theorem Subst.ext_subst (σ τ : Subst φ) (h : ∀t : Term φ, t.subst σ = t.subst τ) : ∀n, σ n = τ n
+  := λn => h (var n)
+
+-- i.e. subst is a faithful functor
+theorem subst_injective : Function.Injective (@subst φ)
+  := λσ τ h => funext (λn => σ.ext_subst τ (λ_ => h ▸ rfl) n)
+
+/-- Create a substitution from a variable renaming -/
+def Subst.fromWk (ρ : ℕ -> ℕ): Subst φ := Term.var ∘ ρ
+
+@[simp]
+theorem Subst.fromWk_apply (ρ : ℕ -> ℕ) (n : ℕ) : (@fromWk φ ρ) n = Term.var (ρ n) := rfl
+
+theorem Subst.fromWk_lift (ρ) : (@fromWk φ ρ).lift = fromWk (Nat.liftWk ρ) := by
+  funext n; cases n <;> rfl
+
+theorem Subst.fromWk_iterate_lift
+  : (n : ℕ) -> ∀ρ, Subst.lift^[n] (@fromWk φ ρ) = fromWk (Nat.liftWk^[n] ρ)
+  | 0, ρ => rfl
+  | n + 1, ρ => by simp [fromWk_lift, fromWk_iterate_lift n]
+
+theorem Subst.fromWk_liftn (n ρ) : (@fromWk φ ρ).liftn n = fromWk (Nat.liftnWk n ρ) := by
+  rw [liftn_eq_iterate_lift, Nat.liftnWk_eq_iterate_liftWk, fromWk_iterate_lift]
+
+theorem subst_fromWk_apply (ρ : ℕ -> ℕ) (t : Term φ) : t.subst (Subst.fromWk ρ) = t.wk ρ := by
+  induction t generalizing ρ <;> simp [Subst.fromWk_liftn, Term.Subst.fromWk_lift,  *]
+
+theorem subst_fromWk (ρ : ℕ -> ℕ) : @Term.subst φ (Subst.fromWk ρ) = Term.wk ρ
+  := funext (subst_fromWk_apply ρ)
+
+theorem subst_comp_fromWk : @Term.subst φ ∘ Subst.fromWk = Term.wk
+  := funext subst_fromWk
+
+theorem subst_liftn (n : ℕ) (σ : Subst φ) (t : Term φ)
+    : (t.wk (Nat.liftnWk n Nat.succ)).subst (σ.liftn (n + 1))
+      = (t.subst (σ.liftn n)).wk (Nat.liftnWk n Nat.succ)
+  := by induction t generalizing σ n with
+  | var =>
+    --TODO: how should this be factored?
+    simp only [wk, subst, Nat.liftnWk, Subst.liftn]
+    split
+    · split
+      · simp [Nat.liftnWk, *]
+      · rename_i H C; exact (C (Nat.le_step H)).elim
+    · rename_i C
+      simp_arith only [ite_false, wk_wk]
+      apply congr
+      · apply congrArg
+        funext v
+        simp_arith [Function.comp_apply, Zero.zero, Nat.liftnWk]
+      · simp [Nat.succ_add, Nat.succ_sub_succ, Nat.add_sub_assoc]
+  | _ => simp [
+    <-Subst.liftn_succ, <-Nat.liftnWk_succ_apply', <-Nat.liftnWk_add_apply', Subst.liftn_liftn', *]
+
+theorem subst_iterate_lift (n : ℕ) (σ : Subst φ) (t : Term φ)
+  : (t.wk (Nat.liftWk^[n] Nat.succ)).subst (Subst.lift^[n + 1] σ)
+    = (t.subst (Subst.lift^[n] σ)).wk (Nat.liftWk^[n] Nat.succ)
+  := by simp only [<-Subst.liftn_eq_iterate_lift, <-Nat.liftnWk_eq_iterate_liftWk, subst_liftn]
+
+theorem subst_lift (t : Term φ) (σ : Subst φ)
+  : (t.wk Nat.succ).subst (σ.lift) = (t.subst σ).wk Nat.succ := t.subst_iterate_lift 0 σ
+
+/-- Compose two substitutions on terms to yield another -/
+def Subst.comp (σ τ : Subst φ): Subst φ
+  | n => (τ n).subst σ
+
+theorem Subst.lift_comp (σ τ : Subst φ) : (σ.comp τ).lift = σ.lift.comp τ.lift := by
+  funext n
+  cases n with
+  | zero => rfl
+  | succ n => simp [lift, comp, Term.subst_lift]
+
+theorem Subst.iterate_lift_comp
+  : (n : ℕ) -> ∀σ τ : Subst φ, Subst.lift^[n] (σ.comp τ)
+    = (Subst.lift^[n] σ).comp (Subst.lift^[n] τ)
+  | 0, σ, τ => rfl
+  | n + 1, σ, τ => by simp [Subst.lift_comp, iterate_lift_comp n]
+
+theorem Subst.liftn_comp (n : ℕ) (σ τ : Subst φ)
+  : (σ.comp τ).liftn n = (σ.liftn n).comp (τ.liftn n)
+  := by rw [liftn_eq_iterate_lift, iterate_lift_comp]
+
+theorem subst_comp (σ τ : Subst φ) (t : Term φ) : t.subst (σ.comp τ) = (t.subst τ).subst σ
+  := by induction t generalizing σ τ with
+  | var => rfl
+  | _ => simp [subst, Subst.lift_comp, Subst.liftn_comp, *]
+
+theorem subst_subst (σ τ : Subst φ) (t : Term φ)
+  : (t.subst τ).subst σ = t.subst (σ.comp τ) := by rw [subst_comp]
+
+@[simp]
+theorem Subst.comp_id (σ : Subst φ) : σ.comp Subst.id = σ := by funext n; rfl
+
+@[simp]
+theorem Subst.id_comp (σ : Subst φ) : Subst.id.comp σ = σ := by funext n; simp [comp]
+
+theorem Subst.comp_assoc (σ τ ρ : Subst φ) : (σ.comp τ).comp ρ = σ.comp (τ.comp ρ) := by
+  funext n
+  simp only [comp, Function.comp_apply, subst_comp]
+
+/-- Substitute a term for the smallest variable, bumping the rest downwards -/
+def subst0 (t : Term φ) : Subst φ
+  | 0 => t
+  | n + 1 => var n
+
+@[simp]
+theorem subst0_zero (t : Term φ) : subst0 t 0 = t := rfl
+
+@[simp]
+theorem subst0_succ (t : Term φ) (n : ℕ) : subst0 t (n + 1) = var n := rfl
+
+theorem subst_subst0_wk (e s : Term φ) (ρ)
+  : (e.subst s.subst0).wk ρ = (e.wk (Nat.liftWk ρ)).subst (s.wk ρ).subst0 := by
+  simp only [<-subst_fromWk_apply, subst_subst]
+  congr
+  funext n
+  cases n <;> rfl
+
+theorem subst0_comp_wk (s : Term φ)
+  : (Subst.fromWk ρ).comp (subst0 s) = (s.wk ρ).subst0.comp (Subst.fromWk (Nat.liftWk ρ))
+  := by funext n; cases n <;> simp [Subst.comp, subst_fromWk_apply]
+
+theorem subst0_var0 : @subst0 φ (var 0) = Subst.fromWk Nat.pred := by funext n; cases n <;> rfl
+
+@[simp]
+theorem wk_succ_comp_subst0 (e : Term φ) : e.subst0.comp (Subst.fromWk Nat.succ) = Subst.id
+  := by funext n; cases n <;> rfl
+
+@[simp]
+theorem wk_succ_subst_subst0 (e s : Term φ) : (e.wk Nat.succ).subst s.subst0 = e := by
+  rw [<-subst_fromWk_apply, <-subst_comp, wk_succ_comp_subst0, subst_id]
+
+@[simp]
+theorem subst0_wk0 (e s : Term φ) : e.wk0.subst s.subst0 = e := wk_succ_subst_subst0 e s
+
+@[simp]
+theorem wk1_subst0_var0 (e : Term φ) : e.wk1.subst (var 0).subst0 = e := by
+  rw [subst0_var0, subst_fromWk, wk1, wk_wk]
+  apply Eq.trans _ e.wk_id
+  congr
+  funext i
+  cases i <;> rfl
+
+@[simp]
+theorem wk1_subst0_var0' (e : Term φ) : (e.wk (Nat.liftWk Nat.succ)).subst (var 0).subst0 = e
+  := e.wk1_subst0_var0
+
+/-- Substitute a term for the `n`th variable, bumping those above it downwards -/
+def substn (n : ℕ) (t : Term φ) : Subst φ := λm =>
+  if m < n then var m else if m = n then t else var (m - 1)
+
+theorem substn_zero (t : Term φ) : substn 0 t = subst0 t := by
+  funext n; cases n <;> rfl
+
+theorem substn_succ (n : ℕ) (t : Term φ)
+  : substn (n + 1) (t.wk Nat.succ) = (substn n t).lift := by
+  funext m
+  cases m with
+  | zero => simp [substn]
+  | succ m =>
+    simp only [substn, Nat.add_lt_add_iff_right, add_left_inj, Nat.add_sub_cancel, Subst.lift]
+    split
+    case isTrue => rfl
+    case isFalse h =>
+      split
+      case isTrue => rfl
+      case isFalse h' =>
+        simp only [wk, Nat.succ_eq_add_one, var.injEq]
+        rw [Nat.sub_add_cancel]
+        exact Nat.succ_le_of_lt $ Nat.lt_of_le_of_lt
+          (Nat.zero_le n)
+          (Nat.lt_of_le_of_ne (Nat.le_of_not_lt h) (Ne.symm h'))
+
+theorem substn_add (n m : ℕ) (t : Term φ)
+  : substn (n + m) (t.wk (· + m)) = (substn n t).liftn m := by
+  induction m with
+  | zero => simp
+  | succ m I => rw [Subst.liftn_succ, <-I, <-substn_succ, <-Nat.add_assoc, wk_wk]; rfl
+
+theorem substn_add_right (n m : ℕ) (t : Term φ)
+  : substn (m + n) (t.wk (· + m)) = (substn n t).liftn m := Nat.add_comm _ _ ▸ substn_add n m t
+
+@[simp]
+theorem substn_n (n : ℕ) (t : Term φ) : substn n t n = t := by simp [substn]
+
+theorem subst_substn_wk (e s : Term φ) (ρ) (n)
+  : (e.subst (s.substn n)).wk (Nat.liftnWk n ρ)
+  = (e.wk (Nat.liftnWk (n + 1) ρ)).subst ((s.wk (Nat.liftnWk n ρ)).substn n) := by
+  simp only [<-subst_fromWk_apply, subst_subst]
+  congr
+  funext k
+  simp only [Subst.fromWk, Subst.comp, wk, substn, subst, Nat.liftnWk]
+  split
+  case isTrue h =>
+    have h' : k < n + 1 := Nat.lt_succ_of_lt h
+    simp only [wk, h, h', Nat.liftnWk, ↓reduceIte]
+    simp only [subst, Function.comp_apply, Nat.liftnWk, var.injEq, ite_eq_left_iff, not_lt]
+    exact λhk => (Nat.not_le_of_lt h hk).elim
+  case isFalse h =>
+    split
+    case isTrue h =>
+      cases h
+      simp
+    case isFalse h' =>
+      have hn : ¬k ≤ n := match Nat.eq_or_lt_of_not_lt h with
+        | Or.inl h => (h' h).elim
+        | Or.inr h => Nat.not_le_of_lt h
+      have h' : ¬k < n + 1 := match Nat.eq_or_lt_of_not_lt h with
+        | Or.inl h => (h' h).elim
+        | Or.inr h => Nat.not_lt_of_le h
+      have h'' : ¬k - 1 < n := λc => (hn (Nat.le_of_pred_lt c)).elim
+      have hρ : ρ (k - 1 - n) = ρ (k - (n + 1)) := by simp [Nat.add_comm n 1, Nat.sub_add_eq]
+      simp_arith [h', h'', Nat.liftnWk, hρ]
+
+theorem liftn_subst0 (n : ℕ) (t : Term φ) : t.subst0.liftn n = (t.wk (· + n)).substn n := by
+  induction n with
+  | zero => simp [substn_zero]
+  | succ n I =>
+    rw [Subst.liftn_succ, I]
+    have h : (· + (n + 1)) = Nat.succ ∘ (· + n) := by funext m; simp_arith
+    rw [h, <-Term.wk_wk, substn_succ]
+
+theorem subst_liftn_subst0_wk (e s : Term φ) (ρ n)
+  : (e.subst (s.subst0.liftn n)).wk (Nat.liftnWk n ρ)
+  = (e.wk (Nat.liftnWk (n + 1) ρ)).subst ((s.wk ρ).subst0.liftn n)
+  := by
+  simp only [liftn_subst0, subst_substn_wk, wk_wk]
+  congr
+  apply congrArg
+  congr
+  funext k
+  simp [Nat.liftnWk]
+
+/-- Substitute a term for the `n`th variable, leaving the rest unchanged -/
+def alpha (n : ℕ) (t : Term φ) : Subst φ := Function.update Subst.id n t
+
+@[simp]
+theorem wk1_comp_subst0 (e : Term φ)
+  : e.subst0.comp (Subst.fromWk (Nat.wkn 1)) = e.alpha 0
+  := by funext n; cases n <;> rfl
+
+@[simp]
+theorem liftWk_succ_comp_subst0 (e : Term φ)
+  : e.subst0.comp (Subst.fromWk (Nat.liftWk Nat.succ)) = e.alpha 0
+  := by funext n; cases n <;> rfl
+
+@[simp]
+theorem wkn_comp_substn_succ (n : ℕ) (e : Term φ)
+  : (e.substn n).comp (Subst.fromWk (Nat.wkn (n + 1))) = e.alpha n := by
+  funext i
+  simp only [Subst.comp, subst, substn, Nat.wkn, alpha, Function.update, eq_rec_constant,
+    Subst.id_apply, dite_eq_ite, Nat.lt_succ_iff]
+  split
+  case isTrue h =>
+    split
+    case isTrue h' => simp [Nat.ne_of_lt h']
+    case isFalse h' => simp [Nat.le_antisymm h (Nat.le_of_not_lt h')]
+  case isFalse h =>
+    have c : ¬(i + 1 < n) := λc => h (Nat.le_of_lt (Nat.lt_trans (by simp) c))
+    have c' : i + 1 ≠ n := λc => by cases c; simp at h
+    have c'' : i ≠ n := λc => h (Nat.le_of_eq c)
+    simp [c, c', c'']
+
+@[simp]
+theorem alpha_var : (var n).alpha n = @Subst.id φ := by funext n; simp [alpha, Subst.id]
+
+theorem wk0_subst {σ : Subst φ} {e : Term φ}
+  : (e.subst σ).wk0 = e.wk0.subst σ.lift := (subst_lift e σ).symm
+
+theorem wk1_subst_lift {σ : Subst φ} {e : Term φ}
+  : (e.subst σ.lift).wk1 = e.wk1.subst σ.lift.lift := by
+  simp only [wk1, <-subst_fromWk, subst_subst]
+  congr
+  funext k
+  cases k with
+  | zero => rfl
+  | succ k =>
+    simp only [
+      Subst.comp, BinSyntax.Term.subst, Nat.liftWk_succ, Nat.succ_eq_add_one, Subst.lift_succ,
+      wk_wk, subst_fromWk, Nat.liftWk_succ_comp_succ
+    ]
+    rfl
+
+theorem wk2_subst_lift_lift {σ : Subst φ} {e : Term φ}
+  : (e.subst σ.lift.lift).wk2 = e.wk2.subst σ.lift.lift.lift := by
+  simp only [wk2, <-subst_fromWk, subst_subst]
+  congr
+  funext k
+  cases k with
+  | zero => rfl
+  | succ k =>
+    cases k with
+    | zero => rfl
+    | succ k =>
+      simp_arith only [
+        Subst.comp, BinSyntax.Term.subst, Nat.liftWk_succ, Nat.succ_eq_add_one, Subst.lift_succ,
+        wk_wk, subst_fromWk, Nat.liftWk_succ_comp_succ, Nat.liftnWk, ↓reduceIte
+      ]
+      rfl
+
+theorem swap01_subst_lift_lift {σ : Subst φ} {e : Term φ}
+  : (e.subst σ.lift.lift).swap01 = e.swap01.subst σ.lift.lift := by
+  simp only [swap01, <-subst_fromWk, subst_subst]
+  congr
+  funext k
+  cases k with
+  | zero => rfl
+  | succ k =>
+    cases k with
+    | zero => rfl
+    | succ k =>
+      simp_arith only [
+        Subst.comp, BinSyntax.Term.subst, Nat.liftWk_succ, Nat.succ_eq_add_one, Subst.lift_succ,
+        wk_wk, subst_fromWk, Nat.liftWk_succ_comp_succ, Nat.liftnWk, ↓reduceIte, Nat.swap0
+      ]
+      rfl
+
+theorem swap02_subst_lift_lift_lift {σ : Subst φ} {e : Term φ}
+  : (e.subst σ.lift.lift.lift).swap02 = e.swap02.subst σ.lift.lift.lift := by
+  simp only [swap02, <-subst_fromWk, subst_subst]
+  congr
+  funext k
+  cases k with
+  | zero => rfl
+  | succ k =>
+    cases k with
+    | zero => rfl
+    | succ k =>
+      cases k with
+      | zero => rfl
+      | succ k =>
+        simp_arith only [
+          Subst.comp, BinSyntax.Term.subst, Nat.liftWk_succ, Nat.succ_eq_add_one, Subst.lift_succ,
+          wk_wk, subst_fromWk, Nat.liftWk_succ_comp_succ, Nat.liftnWk, ↓reduceIte, Nat.swap0
+        ]
+        rfl
+
+end Term
+
+/-- Substitute the free variables in a body -/
+@[simp]
+def Body.subst (σ : Term.Subst φ) : Body φ → Body φ
+  | nil => nil
+  | let1 e t => let1 (e.subst σ) (t.subst σ.lift)
+  | let2 e t => let2 (e.subst σ) (t.subst (σ.liftn 2))
+
+@[simp]
+theorem Body.subst_id (b : Body φ) : b.subst Term.Subst.id = b := by
+  induction b <;> simp [Term.Subst.lift_id, Term.Subst.liftn_id, *]
+
+theorem Body.subst_comp (σ τ : Term.Subst φ) (b : Body φ)
+  : b.subst (σ.comp τ) = (b.subst τ).subst σ := by
+  induction b generalizing σ τ
+  <;> simp [Term.subst_comp, Term.Subst.lift_comp, Term.Subst.liftn_comp, *]
+
+@[simp]
+theorem Body.num_defs_subst (σ : Term.Subst φ) (b : Body φ)
+  : (b.subst σ).num_defs = b.num_defs := by
+  induction b generalizing σ <;> simp [*]
+
+/-- Substitute the free variables in a `Terminator` using `σ` -/
+@[simp]
+def Terminator.vsubst (σ : Term.Subst φ) : Terminator φ → Terminator φ
+  | br ℓ e => br ℓ (e.subst σ)
+  | case e s t => case (e.subst σ) (vsubst σ.lift s) (vsubst σ.lift t)
+
+@[simp]
+theorem Terminator.vsubst_id (r : Terminator φ) : r.vsubst Term.Subst.id = r := by
+  induction r <;> simp [*]
+
+theorem Terminator.vsubst_vsubst (σ τ : Term.Subst φ) (r : Terminator φ)
+  : (r.vsubst τ).vsubst σ = r.vsubst (σ.comp τ) := by
+  induction r generalizing σ τ
+  <;> simp [Term.subst_comp, Term.Subst.lift_comp, Term.Subst.liftn_comp, *]
+
+theorem Terminator.ext_vsubst (σ τ : Term.Subst φ)
+  (h : ∀t : Terminator φ, t.vsubst σ = t.vsubst τ) : ∀n, σ n = τ n
+  := λn => by
+    have h' := h (br 0 (Term.var n))
+    simp at h'
+    exact h'
+
+-- i.e. vsubst is a faithful functor
+theorem Terminator.vsubst_injective : Function.Injective (@Terminator.vsubst φ)
+  := λσ τ h => funext (λn => Terminator.ext_vsubst σ τ (λ_ => h ▸ rfl) n)
+
+theorem Terminator.vsubst_fromWk_apply (ρ : ℕ -> ℕ) (r : Terminator φ)
+  : r.vsubst (Term.Subst.fromWk ρ) = r.vwk ρ := by
+  induction r generalizing ρ
+  <;> simp [Term.subst_fromWk_apply, Term.Subst.fromWk_liftn, Term.Subst.fromWk_lift, *]
+
+theorem Terminator.vsubst_fromWk (ρ : ℕ -> ℕ)
+  : vsubst (Term.Subst.fromWk ρ) = @vwk φ ρ := funext (vsubst_fromWk_apply ρ)
+
+theorem Terminator.vsubst_comp_fromWk
+  : @vsubst φ ∘ Term.Subst.fromWk = @vwk φ := funext vsubst_fromWk
+
+theorem Terminator.lwk_vsubst (σ : Term.Subst φ) (ρ : ℕ -> ℕ) (r : Terminator φ)
+  : (r.vsubst σ).lwk ρ = (r.lwk ρ).vsubst σ := by induction r generalizing σ <;> simp [*]
+
+theorem Terminator.vsubst_lwk (σ : Term.Subst φ) (ρ : ℕ -> ℕ) (r : Terminator φ)
+  : (r.lwk ρ).vsubst σ = (r.vsubst σ).lwk ρ := Eq.symm $ Terminator.lwk_vsubst σ ρ r
+
+@[simp]
+theorem Terminator.vwk_succ_vsubst_subst0 (t : Terminator φ) (s : Term φ)
+  : (t.vwk Nat.succ).vsubst s.subst0 = t := by
+  rw [<-vsubst_fromWk_apply, vsubst_vsubst, Term.wk_succ_comp_subst0, vsubst_id]
+
+/-- Substitute the free variables in a basic block -/
+@[simp]
+def Block.vsubst (σ : Term.Subst φ) (β : Block φ) : Block φ where
+  body := β.body.subst σ
+  terminator := β.terminator.vsubst (σ.liftn β.body.num_defs)
+
+@[simp]
+theorem Block.vsubst_id (β : Block φ) : β.vsubst Term.Subst.id = β := by simp
+
+theorem Block.vsubst_vsubst (σ τ : Term.Subst φ) (β : Block φ)
+  : (β.vsubst τ).vsubst σ = β.vsubst (σ.comp τ)
+  := by simp [
+    Body.subst_comp, Body.num_defs_subst, Term.Subst.liftn_comp, Terminator.vsubst_vsubst, *]
+
+/-- Substitute the free variables in a region -/
+@[simp]
+def BBRegion.vsubst (σ : Term.Subst φ) : BBRegion φ → BBRegion φ
+  | cfg β n f => cfg (β.vsubst σ) n (λ i => (f i).vsubst (σ.liftn (β.body.num_defs + 1)))
+
+@[simp]
+theorem BBRegion.vsubst_id (r : BBRegion φ) : r.vsubst Term.Subst.id = r := by
+  induction r; simp [*]
+
+theorem BBRegion.vsubst_vsubst (σ τ : Term.Subst φ) (r : BBRegion φ)
+  : (r.vsubst τ).vsubst σ = r.vsubst (σ.comp τ) := by
+  induction r generalizing σ τ
+  simp [Body.subst_comp, Body.num_defs_subst, Term.Subst.liftn_comp, Terminator.vsubst_vsubst, *]
+
+/-- Substitute the free variables in a control-flow graph -/
+@[simp]
+def BBCFG.vsubst (σ : Term.Subst φ) (cfg : BBCFG φ) : BBCFG φ where
+  length := cfg.length
+  targets := λi => (cfg.targets i).vsubst σ
+
+@[simp]
+theorem BBCFG.vsubst_id (cfg : BBCFG φ) : cfg.vsubst Term.Subst.id = cfg := by
+  cases cfg; simp [*]
+
+theorem BBCFG.vsubst_vsubst (σ τ : Term.Subst φ) (cfg : BBCFG φ)
+  : (cfg.vsubst τ).vsubst σ = cfg.vsubst (σ.comp τ) := by
+  cases cfg; simp [BBRegion.vsubst_vsubst, *]
+
+/-- Substitute the free variables in a region -/
+@[simp]
+def TRegion.vsubst (σ : Term.Subst φ) : TRegion φ → TRegion φ
+  | let1 e t => let1 (e.subst σ) (t.vsubst σ.lift)
+  | let2 e t => let2 (e.subst σ) (t.vsubst (σ.liftn 2))
+  | cfg β n f => cfg (β.vsubst σ) n (λ i => (f i).vsubst σ.lift)
+
+@[simp]
+theorem TRegion.vsubst_id (r : TRegion φ) : r.vsubst Term.Subst.id = r := by
+  induction r <;> simp [TRegion.vsubst, Term.Subst.lift_id, Term.Subst.liftn_id, *]
+
+theorem TRegion.vsubst_vsubst (σ τ : Term.Subst φ) (r : TRegion φ)
+  : (r.vsubst τ).vsubst σ = r.vsubst (σ.comp τ) := by
+  induction r generalizing σ τ
+  <;> simp [Term.subst_comp, Terminator.vsubst_vsubst, Term.Subst.lift_comp, Term.Subst.liftn_comp, *]
+
+def TCFG.vsubst (σ : Term.Subst φ) (cfg : TCFG φ) : TCFG φ where
+  length := cfg.length
+  targets := λi => (cfg.targets i).vsubst σ
+
+@[simp]
+theorem TCFG.vsubst_id (cfg : TCFG φ) : cfg.vsubst Term.Subst.id = cfg := by
+  cases cfg; simp [TCFG.vsubst, *]
+
+theorem TCFG.vsubst_vsubst (σ τ : Term.Subst φ) (cfg : TCFG φ)
+  : (cfg.vsubst τ).vsubst σ = cfg.vsubst (σ.comp τ) := by
+  cases cfg; simp [TCFG.vsubst, TRegion.vsubst_vsubst, *]
+
+/-- Substitute the free variables in a `Region` using `σ` -/
+@[simp]
+def Region.vsubst (σ : Term.Subst φ) : Region φ → Region φ
+  | br n e => br n (e.subst σ)
+  | case e s t => case (e.subst σ) (vsubst σ.lift s) (vsubst σ.lift t)
+  | let1 e t => let1 (e.subst σ) (vsubst σ.lift t)
+  | let2 e t => let2 (e.subst σ) (vsubst (σ.liftn 2) t)
+  | cfg β n f => cfg (vsubst σ β) n (λ i => (f i).vsubst σ.lift)
+
+@[simp]
+theorem Region.vsubst_id (r : Region φ) : r.vsubst Term.Subst.id = r := by
+  induction r <;> simp [*]
+
+theorem Region.vsubst_id' (r : Region φ) (h : σ = Term.Subst.id) : r.vsubst σ = r := by
+  cases h; simp
+
+theorem Region.vsubst_comp_apply (σ τ : Term.Subst φ) (r : Region φ)
+  : r.vsubst (σ.comp τ) = (r.vsubst τ).vsubst σ := by
+  induction r generalizing σ τ
+  <;> simp [Term.subst_comp, Term.Subst.lift_comp, Term.Subst.liftn_comp, *]
+
+theorem Region.vsubst_vsubst (σ τ : Term.Subst φ) (r : Region φ)
+  : (r.vsubst τ).vsubst σ = r.vsubst (σ.comp τ) := by
+  induction r generalizing σ τ
+  <;> simp [Term.subst_comp, Term.Subst.lift_comp, Term.Subst.liftn_comp, *]
+
+theorem Region.vsubst_comp (σ τ : Term.Subst φ)
+  : vsubst σ ∘ vsubst τ = vsubst (σ.comp τ) := by
+  funext r; simp [vsubst_vsubst]
+
+theorem Region.ext_vsubst (σ τ : Term.Subst φ)
+  (h : ∀t : Region φ, t.vsubst σ = t.vsubst τ) : ∀n, σ n = τ n
+  := λn => by
+    have h' := h (br 0 (Term.var n))
+    simp at h'
+    exact h'
+
+theorem Region.vsubst_cfg (σ : Term.Subst φ) (β : Region φ) (n : ℕ) (G : Fin n -> Region φ)
+  : (cfg β n G).vsubst σ = cfg (β.vsubst σ) n (λi => (G i).vsubst σ.lift) := rfl
+
+theorem Region.vsubst_cfg1 (σ : Term.Subst φ) (β : Region φ) (G : Region φ)
+  : (cfg β 1 (Fin.elim1 G)).vsubst σ = cfg (β.vsubst σ) 1 (Fin.elim1 (G.vsubst σ.lift)) := by
+  simp only [vsubst, cfg.injEq, heq_eq_eq, true_and]
+  funext i; cases i using Fin.elim1; rfl
+
+-- i.e. vsubst is a faithful functor
+theorem Region.vsubst_injective : Function.Injective (@Region.vsubst φ)
+  := λσ τ h => funext (λn => Region.ext_vsubst σ τ (λ_ => h ▸ rfl) n)
+
+theorem Region.vsubst_fromWk_apply (ρ : ℕ -> ℕ) (r : Region φ)
+  : r.vsubst (Term.Subst.fromWk ρ) = r.vwk ρ := by
+  induction r generalizing ρ
+  <;> simp [Term.subst_fromWk_apply, Term.Subst.fromWk_liftn, Term.Subst.fromWk_lift, *]
+
+theorem Region.vsubst_fromWk (ρ : ℕ -> ℕ)
+  : vsubst (Term.Subst.fromWk ρ) = @vwk φ ρ := funext (vsubst_fromWk_apply ρ)
+
+theorem Region.vsubst0_var0_vwk1 (r : Region φ)
+  : r.vwk1.vsubst (Term.subst0 (Term.var 0)) = r := by
+  rw [vwk1, <-vsubst_fromWk, vsubst_vsubst, vsubst_id']
+  funext k; cases k <;> rfl
+
+theorem Region.vsubst_comp_fromWk
+  : @vsubst φ ∘ Term.Subst.fromWk = @vwk φ := funext vsubst_fromWk
+
+theorem Region.vsubst0_var0_comp_vwk1
+  : vsubst (Term.subst0 (Term.var 0)) ∘ vwk1 (φ := φ) = id
+  := funext vsubst0_var0_vwk1
+
+theorem Region.lwk_vsubst (σ : Term.Subst φ) (ρ : ℕ -> ℕ) (r : Region φ)
+  : (r.vsubst σ).lwk ρ = (r.lwk ρ).vsubst σ := by induction r generalizing σ ρ <;> simp [*]
+
+theorem Region.vsubst_lwk (σ : Term.Subst φ) (ρ : ℕ -> ℕ) (r : Region φ)
+  : (r.lwk ρ).vsubst σ = (r.vsubst σ).lwk ρ := Eq.symm $ Region.lwk_vsubst σ ρ r
+
+theorem Region.lwk1_vsubst (σ : Term.Subst φ) (r : Region φ)
+  : (r.vsubst σ).lwk1 = (r.lwk1).vsubst σ := by rw [lwk1, lwk_vsubst]
+
+theorem Region.vsubst_lwk1 (σ : Term.Subst φ) (r : Region φ)
+  : (r.lwk1).vsubst σ = (r.vsubst σ).lwk1 := by rw [lwk1, vsubst_lwk]
+
+/-- Substitute the free variables in a `CFG` using `σ` -/
+def CFG.vsubst (σ : Term.Subst φ) (G : CFG φ) : CFG φ where
+  length := G.length
+  targets := λ i => (G.targets i).vsubst σ
+
+@[simp]
+theorem CFG.vsubst_id (G : CFG φ) : G.vsubst Term.Subst.id = G := by cases G; simp [vsubst]
+
+theorem CFG.vsubst_comp_apply (σ τ : Term.Subst φ) (G : CFG φ) : G.vsubst (σ.comp τ) = (G.vsubst τ).vsubst σ
+  := by cases G; simp only [CFG.vsubst, Region.vsubst_comp_apply, *]
diff --git a/DeBruijnSSA/BinSyntax/Syntax/Subst/Terminator.lean b/DeBruijnSSA/BinSyntax/Syntax/Subst/Terminator.lean
new file mode 100644
index 0000000..da5fab7
--- /dev/null
+++ b/DeBruijnSSA/BinSyntax/Syntax/Subst/Terminator.lean
@@ -0,0 +1,428 @@
+import Discretion.Wk.Nat
+import Discretion.Wk.Fin
+import Discretion.Wk.Multiset
+import Discretion.Wk.Multiset
+
+import DeBruijnSSA.BinSyntax.Syntax.Subst.Term
+
+namespace BinSyntax
+
+/-! ### Terminator substitutions
+ -/
+namespace Terminator
+
+/-- A substitution mapping labels to terminators -/
+def Subst (φ : Type _) := ℕ → Terminator φ
+
+/-- The identity substitution, which maps labels to themselves -/
+def Subst.id : Subst φ := λn => Terminator.br n (Term.var 0)
+
+theorem Subst.id_apply (n : ℕ) : @Subst.id φ n = Terminator.br n (Term.var 0) := rfl
+
+/-- Lift a substitution under a label binder -/
+def Subst.lift (σ : Subst φ) : Subst φ
+  | 0 => Terminator.br 0 (Term.var 0)
+  | n + 1 => (σ n).lwk Nat.succ
+
+/-- Lift a substitution under `n` label binders -/
+def Subst.liftn (n : ℕ) (σ : Subst φ) : Subst φ
+  := λm => if m < n then Terminator.br m (Term.var 0) else (σ (m - n)).lwk (λv => v + n)
+
+@[simp]
+theorem Subst.liftn_zero (σ : Subst φ) : σ.liftn 0 = σ := by
+  funext n
+  simp only [liftn]
+  split
+  · rename_i H; cases H
+  · exact (σ n).lwk_id
+
+theorem Subst.liftn_one (σ : Subst φ) : σ.liftn 1 = σ.lift := by funext m; cases m <;> rfl
+
+theorem Subst.liftn_succ (n) (σ: Subst φ) : σ.liftn n.succ = (σ.liftn n).lift := by
+  induction n with
+  | zero => rw [σ.liftn_one, σ.liftn_zero]
+  | succ n I => -- TODO: I'm sure this can be made _much_ cleaner...
+    funext m
+    rw [I]
+    simp only [lift]
+    split
+    · rfl
+    · simp only [liftn]
+      split
+      · split
+        · rfl
+        · split
+          · rfl
+          · rename_i H C; exact (C (Nat.lt_of_succ_lt_succ (Nat.lt_of_succ_lt_succ H))).elim
+      · split
+        · rename_i H; simp_arith at H
+        · split
+          · rename_i C H; exact (C (Nat.succ_lt_succ (Nat.succ_lt_succ H))).elim
+          · simp only [Terminator.lwk_lwk]
+            apply congr
+            apply congrArg
+            funext v
+            simp_arith
+            simp_arith
+
+theorem Subst.liftn_two (σ : Subst φ) : σ.liftn 2 = σ.lift.lift := by
+  rw [Subst.liftn_succ, Subst.liftn_succ]; simp
+
+theorem Subst.liftn_eq_iterate_lift_apply (n: ℕ) (σ: Subst φ) : σ.liftn n = (Subst.lift^[n] σ)
+  := by induction n with
+  | zero => exact σ.liftn_zero
+  | succ n => simp only [Function.iterate_succ_apply', Subst.liftn_succ, *]
+
+theorem Subst.liftn_eq_iterate_lift (n: ℕ) : Subst.liftn n = (@Subst.lift φ)^[n] := by
+  funext σ
+  rw [liftn_eq_iterate_lift_apply]
+
+theorem Subst.liftn_succ' (n) (σ: Subst φ) : σ.liftn n.succ = σ.lift.liftn n := by
+  simp [liftn_eq_iterate_lift]
+
+@[simp]
+theorem Subst.lift_id : (@id φ).lift = id := by funext n; cases n <;> rfl
+
+@[simp]
+theorem Subst.iterate_lift_id : (n: ℕ) -> Subst.lift^[n] (@id φ) = id
+  | 0 => rfl
+  | n + 1 => by simp [lift_id, iterate_lift_id n]
+
+@[simp]
+theorem Subst.liftn_id (n: ℕ): (@id φ).liftn n = id := by
+  rw [liftn_eq_iterate_lift_apply, iterate_lift_id]
+
+theorem Subst.liftn_add (n m: ℕ) : Subst.liftn (m + n) = (@Subst.liftn α m) ∘ (@Subst.liftn α n)
+  := by simp [liftn_eq_iterate_lift, Function.iterate_add]
+
+theorem Subst.liftn_liftn (n m: ℕ) (σ: Subst φ): (σ.liftn n).liftn m = σ.liftn (m + n)
+  := by simp [liftn_add]
+
+theorem Subst.lift_succ (σ : Subst φ) (i : ℕ) : σ.lift (i + 1) = (σ i).lwk Nat.succ := rfl
+
+/-- Lift a substitution under a variable binder -/
+def Subst.vlift (σ : Subst φ) : Subst φ := vwk1 ∘ σ
+
+@[simp]
+theorem Subst.vlift_id : (@id φ).vlift = id := by funext v; cases v <;> rfl
+
+theorem Subst.vlift_lift_comm (σ : Subst σ) : σ.lift.vlift = σ.vlift.lift := by
+  funext n
+  cases n with
+  | zero => rfl
+  | succ n => simp [Subst.vlift, lift, vwk_lwk, vwk1]
+
+theorem Subst.vlift_lift_comp_comm : Subst.vlift ∘ (@Subst.lift φ) = Subst.lift ∘ Subst.vlift
+  := funext Subst.vlift_lift_comm
+
+theorem Subst.vlift_liftn_comm (n : ℕ) (σ : Subst σ) : (σ.liftn n).vlift = σ.vlift.liftn n := by
+  induction n generalizing σ with
+  | zero => simp
+  | succ _ I => rw [liftn_succ, vlift_lift_comm, I, liftn_succ]
+
+/-- Lift a substitution under `n` variable binders -/
+def Subst.vliftn (n : ℕ) (σ : Subst φ) : Subst φ
+  := Terminator.vwk (Nat.liftWk (λi => i + n)) ∘ σ
+
+@[simp]
+theorem Subst.vliftn_zero (σ : Subst φ) : σ.vliftn 0 = σ := by
+  funext n
+  simp [vliftn]
+
+theorem Subst.vliftn_one (σ : Subst φ) : σ.vliftn 1 = σ.vlift := by
+  funext n
+  simp [vliftn, vlift, vwk1]
+
+theorem Subst.vliftn_succ (σ : Subst φ) (i : ℕ) : σ.vliftn (i + 1) = (σ.vliftn i).vlift := by
+  funext ℓ
+  simp only [vliftn, Function.comp_apply, vlift, vwk_vwk, vwk1]
+  congr
+  funext n
+  cases n <;> rfl
+
+theorem Subst.vliftn_two (σ : Subst φ) : σ.vliftn 2 = σ.vlift.vlift := by
+  rw [Subst.vliftn_succ, Subst.vliftn_succ]; simp
+
+theorem Subst.vliftn_eq_iterate_vlift_apply (n: ℕ) (σ: Subst φ) : σ.vliftn n = (Subst.vlift^[n] σ)
+  := by induction n with
+  | zero => exact σ.vliftn_zero
+  | succ n => simp only [Function.iterate_succ_apply', Subst.vliftn_succ, *]
+
+theorem Subst.vliftn_eq_iterate_vlift (n: ℕ) : Subst.vliftn n = (@Subst.vlift φ)^[n] := by
+  funext σ
+  rw [vliftn_eq_iterate_vlift_apply]
+
+theorem Subst.vliftn_succ' (σ : Subst φ) (i : ℕ) : σ.vliftn (i + 1) = σ.vlift.vliftn i
+  := by simp [vliftn_eq_iterate_vlift]
+
+theorem Subst.vliftn_add (σ : Subst φ) (n m: ℕ) : σ.vliftn (n + m) = (σ.vliftn m).vliftn n := by
+  funext k
+  simp [vliftn_eq_iterate_vlift, Function.iterate_add_apply]
+
+theorem Subst.iterate_vlift_id : (n: ℕ) -> Subst.vlift^[n] (@id φ) = id
+  | 0 => rfl
+  | n + 1 => by simp [Subst.vlift_id, iterate_vlift_id n]
+
+theorem Subst.vliftn_id (n: ℕ): (@id φ).vliftn n = id := by
+  rw [vliftn_eq_iterate_vlift_apply, iterate_vlift_id]
+
+theorem Subst.iterate_vlift_liftn_comm (k n : ℕ) (σ: Subst φ)
+  : Subst.vlift^[k] (σ.liftn n) = (Subst.vlift^[k] σ).liftn n := by
+  induction k generalizing σ with
+  | zero => rfl
+  | succ n I => simp [I, vlift_liftn_comm]
+
+theorem Subst.vliftn_liftn (k n : ℕ) (σ: Subst φ)
+  : (σ.liftn n).vliftn k = (σ.vliftn k).liftn n
+  := by simp [vliftn_eq_iterate_vlift, iterate_vlift_liftn_comm]
+
+theorem Subst.liftn_vliftn (k n : ℕ) (σ: Subst φ)
+  : (σ.vliftn k).liftn n = (σ.liftn n).vliftn k
+  := by simp [vliftn_eq_iterate_vlift, iterate_vlift_liftn_comm]
+
+/-- Substitute the labels in a `Terminator` using `σ` -/
+@[simp]
+def lsubst (σ : Subst φ) : Terminator φ → Terminator φ
+  | Terminator.br n e => (σ n).vsubst e.subst0
+  | Terminator.case e s t => Terminator.case e (lsubst σ.vlift s) (lsubst σ.vlift t)
+
+theorem lsubst_id_apply (t : Terminator φ) : t.lsubst Subst.id = t
+  := by induction t <;> simp [*]
+
+@[simp]
+theorem lsubst_id : @lsubst φ (Subst.id) = id := funext lsubst_id_apply
+
+theorem lsubst_id_apply' (t : Terminator φ) : t.lsubst (λi => Terminator.br i (Term.var 0)) = t
+  := t.lsubst_id_apply
+
+@[simp]
+theorem lsubst_id' : @lsubst φ (λi => Terminator.br i (Term.var 0)) = id := funext lsubst_id_apply'
+
+/-- Create a substitution from a label renaming -/
+def Subst.fromLwk (ρ : ℕ -> ℕ): Subst φ := λn => Terminator.br (ρ n) (Term.var 0)
+
+theorem Subst.vwk_lift_comp_fromLwk (ρ σ) : vwk (Nat.liftWk ρ) ∘ fromLwk σ = @fromLwk φ σ := rfl
+
+theorem Subst.vwk1_comp_fromLwk (σ) : vwk1 ∘ fromLwk σ = @fromLwk φ σ := rfl
+
+@[simp]
+theorem Subst.fromLwk_vlift (ρ) : (@fromLwk φ ρ).vlift = fromLwk ρ := rfl
+
+@[simp]
+theorem Subst.fromLwk_iterate_vlift (n : ℕ) (ρ)
+  : Subst.vlift^[n] (@fromLwk φ ρ) = fromLwk ρ
+  := by induction n <;> simp [fromLwk_vlift, *]
+
+@[simp]
+theorem Subst.fromLwk_vliftn (n ρ) : (@fromLwk φ ρ).vliftn n = fromLwk ρ := by
+  rw [vliftn_eq_iterate_vlift, fromLwk_iterate_vlift]
+
+@[simp]
+theorem Subst.fromLwk_apply (ρ : ℕ -> ℕ) (n : ℕ)
+  : (@fromLwk φ ρ) n = Terminator.br (ρ n) (Term.var 0) := rfl
+
+theorem Subst.fromLwk_lift (ρ) : (@fromLwk φ ρ).lift = fromLwk (Nat.liftWk ρ) := by
+  funext n; cases n <;> rfl
+
+theorem Subst.fromLwk_iterate_lift (n : ℕ) (ρ)
+  : Subst.lift^[n] (@fromLwk φ ρ) = fromLwk (Nat.liftWk^[n] ρ)
+  := by induction n generalizing ρ <;> simp [fromLwk_lift, *]
+
+theorem Subst.fromLwk_liftn (n ρ) : (@fromLwk φ ρ).liftn n = fromLwk (Nat.liftnWk n ρ) := by
+  rw [liftn_eq_iterate_lift, Nat.liftnWk_eq_iterate_liftWk, fromLwk_iterate_lift]
+
+theorem lsubst_fromLwk_apply (ρ : ℕ -> ℕ) (t : Terminator φ)
+  : t.lsubst (Subst.fromLwk ρ) = t.lwk ρ := by
+  induction t generalizing ρ
+  <;> simp [Terminator.lsubst, Terminator.lwk, Term.subst_fromWk_apply, *]
+
+theorem lsubst_fromLwk (ρ : ℕ -> ℕ) : lsubst (Subst.fromLwk ρ) = @lwk φ ρ
+  := funext (lsubst_fromLwk_apply ρ)
+
+theorem lsubst_comp_fromLwk : @lsubst φ ∘ (@Subst.fromLwk φ) = lwk := funext lsubst_fromLwk
+
+theorem lsubst_liftn (n : ℕ) (σ : Subst φ) (t : Terminator φ)
+    : (t.lwk (Nat.liftnWk n Nat.succ)).lsubst (σ.liftn (n + 1))
+      = (t.lsubst (σ.liftn n)).lwk (Nat.liftnWk n Nat.succ)
+  := by induction t generalizing σ n with
+  | br ℓ e =>
+    simp only [lwk, lsubst, Nat.liftnWk, Subst.liftn]
+    split
+    · split
+      · simp [lwk, Nat.liftnWk, *]
+      · rename_i H C; exact (C (Nat.le_step H)).elim
+    · rename_i C
+      simp_arith only [ite_false]
+      rw [Nat.succ_eq_add_one]
+      have h : ℓ - n + 1 + n - (n + 1) = ℓ - n := by
+        rw [Nat.add_assoc, Nat.add_comm 1 n, Nat.add_sub_cancel]
+      rw [h, Terminator.lwk_vsubst, lwk_lwk]
+      congr
+      funext n
+      simp_arith [Nat.liftnWk]
+  | case e s t => simp [Subst.vlift_liftn_comm, *]
+
+theorem lsubst_iterate_lift (n : ℕ) (σ : Subst φ) (t : Terminator φ)
+  : (t.lwk (Nat.liftWk^[n] Nat.succ)).lsubst (Subst.lift^[n + 1] σ)
+    = (t.lsubst (Subst.lift^[n] σ)).lwk (Nat.liftWk^[n] Nat.succ)
+  := by simp only [<-Subst.liftn_eq_iterate_lift, <-Nat.liftnWk_eq_iterate_liftWk, lsubst_liftn]
+
+theorem lsubst_lift (t : Terminator φ) (σ : Subst φ)
+  : (t.lwk Nat.succ).lsubst (σ.lift) = (t.lsubst σ).lwk Nat.succ := t.lsubst_iterate_lift 0 σ
+
+/-- Compose two label-substitutions to yield another -/
+def Subst.comp (σ τ : Subst φ): Subst φ
+  | n => (τ n).lsubst σ.vlift
+
+@[simp]
+theorem Subst.comp_id (σ : Subst φ) : σ.comp Subst.id = σ := by
+  funext n
+  simp only [comp, Terminator.lsubst, Function.comp_apply, vlift, vwk1]
+  rw [<-Terminator.vsubst_fromWk_apply, Terminator.vsubst_vsubst]
+  simp
+
+@[simp]
+theorem Subst.id_comp (σ : Subst φ) : Subst.id.comp σ = σ
+  := by funext n; exact lsubst_id_apply (σ n)
+
+theorem Subst.vlift_comp_liftWk_stepn (σ : Subst φ) (n)
+  : vlift (vwk (Nat.liftWk (· + n)) ∘ σ) = vwk (Nat.liftWk (· + n)) ∘ σ.vlift := by
+  simp only [vlift, vwk1, <-Function.comp.assoc]
+  apply congrArg₂
+  funext i
+  simp only [Function.comp_apply, vwk_vwk]
+  apply congrArg₂
+  funext i
+  simp only [Function.comp_apply, Nat.wkn]
+  cases i <;> simp_arith
+  rfl
+  rfl
+
+theorem Subst.vlift_comp_liftWk_succ (σ : Subst φ)
+  : vlift (vwk (Nat.liftWk Nat.succ) ∘ σ) = vwk (Nat.liftWk Nat.succ) ∘ σ.vlift
+  := rfl
+
+theorem Subst.vlift_comp_wk1 (σ : Subst φ)
+  : vlift (vwk (Nat.wkn 1) ∘ σ) = vwk (Nat.wkn 1) ∘ σ.vlift
+  := Nat.wkn_one ▸ vlift_comp_liftWk_succ σ
+
+theorem vsubst_substn_lsubst_vliftn (t : Terminator φ) (e : Term φ) (σ : Subst φ) (n)
+  : (t.lsubst (σ.vliftn (n + 1))).vsubst (e.substn n)
+  = (t.vsubst (e.substn n)).lsubst (σ.vliftn n)
+  := by induction t generalizing σ e n with
+  | br ℓ e' =>
+    simp only [
+      lsubst, Subst.vliftn, <-Terminator.vsubst_fromWk, Terminator.vsubst_vsubst,
+      Function.comp_apply]
+    congr
+    funext k
+    cases k with
+    | zero => rfl
+    | succ k => simp_arith [Term.Subst.comp, Term.subst, Term.substn, Nat.liftWk]
+  | _ => simp only [vsubst, lsubst,  <-Subst.vliftn_succ, <-Term.substn_succ, *]
+
+theorem vsubst_subst0_lsubst_vlift (t : Terminator φ) (e : Term φ) (σ : Subst φ)
+    : (t.lsubst σ.vlift).vsubst e.subst0 = (t.vsubst e.subst0).lsubst σ := by
+  have h := vsubst_substn_lsubst_vliftn t e σ 0
+  simp only [Term.substn_zero, Subst.vliftn_zero, Subst.vliftn_one, Nat.zero_add] at h
+  exact h
+
+theorem vsubst_substn_vwk (t : Terminator φ) (e : Term φ) (ρ n)
+  : (t.vsubst (e.substn n)).vwk (Nat.liftnWk n ρ)
+  = (t.vwk (Nat.liftnWk (n + 1) ρ)).vsubst ((e.wk (Nat.liftnWk n ρ)).substn n)
+  := by induction t generalizing e ρ n with
+  | br ℓ e' => simp only [vwk, vsubst, Term.subst_substn_wk]
+  | _ => simp [
+    <-Nat.liftnWk_succ_apply',
+    <-Term.substn_succ, Term.subst_substn_wk,
+    Term.wk_wk, Nat.liftnWk_comp_succ, *]
+
+theorem vsubst_subst0_vwk (t : Terminator φ) (e : Term φ) (ρ)
+  : (t.vsubst e.subst0).vwk ρ = (t.vwk (Nat.liftWk ρ)).vsubst (e.wk ρ).subst0 := by
+  have h := vsubst_substn_vwk t e ρ 0
+  simp [Nat.liftnWk_one, Nat.liftnWk_zero, Term.substn_zero] at h
+  exact h
+
+theorem vwk_lsubst (σ ρ) (t : Terminator φ)
+  : (t.lsubst σ).vwk ρ = (t.vwk ρ).lsubst (vwk (Nat.liftWk ρ) ∘ σ)
+  := by induction t generalizing σ ρ with
+  | br ℓ e => simp [vsubst_subst0_vwk]
+  | _ =>
+    simp only [vwk, lsubst, *]
+    congr <;> simp only [
+      Subst.vlift, vwk1, <-Function.comp.assoc, <-vwk_comp, <-Nat.liftWk_comp, Nat.liftWk_comp_succ
+    ]
+
+theorem Subst.vliftn_comp (n : ℕ) (σ τ : Subst φ)
+  : (σ.comp τ).vliftn n = (σ.vliftn n).comp (τ.vliftn n)
+  := by
+  funext m
+  simp only [Function.comp_apply, comp, vlift, vliftn, vwk1, Function.comp_apply]
+  generalize τ m = t
+  rw [vwk_lsubst]
+  simp only [<-Function.comp.assoc, <-vwk_comp, <-Nat.liftWk_comp, Nat.liftWk_comp_succ]
+
+theorem Subst.vlift_comp (σ τ : Subst φ) : (σ.comp τ).vlift = σ.vlift.comp τ.vlift
+  := σ.vliftn_comp 1 τ
+
+theorem lsubst_lsubst (σ τ : Subst φ) (t : Terminator φ)
+  : (t.lsubst τ).lsubst σ = t.lsubst (σ.comp τ)
+  := by induction t generalizing σ τ with
+  | br ℓ e => simp only [lsubst, Subst.comp, vsubst_subst0_lsubst_vlift]
+  | case e s t Is It => simp only [lsubst, Subst.comp, Subst.vlift_comp, *]
+
+theorem lsubst_comp (σ τ : Subst φ)
+  : Terminator.lsubst (σ.comp τ) = Terminator.lsubst σ ∘ Terminator.lsubst τ
+  := Eq.symm $ funext $ lsubst_lsubst σ τ
+
+theorem Subst.liftn_comp (n : ℕ) (σ τ : Subst φ) : (σ.comp τ).liftn n = (σ.liftn n).comp (τ.liftn n)
+  := by
+  funext k
+  simp only [liftn, comp]
+  split
+  case isTrue h => simp [liftn, vlift, h]
+  case isFalse h =>
+    simp only [vlift, ←lsubst_fromLwk_apply, lsubst_lsubst]
+    congr
+    funext k
+    simp only [comp, vlift, vwk1, vwk_lift_comp_fromLwk, Function.comp_apply, lsubst_fromLwk_apply,
+      lsubst, Term.subst0_var0, liftn, Nat.add_sub_cancel, vwk_vwk, vsubst_fromWk_apply]
+    rw [ite_cond_eq_false]
+    simp only [vwk_lwk]
+    congr
+    funext k
+    cases k <;> rfl
+    simp_arith
+
+theorem Subst.lift_comp (σ τ : Subst φ) : (σ.comp τ).lift = σ.lift.comp τ.lift := by
+  have h := Subst.liftn_comp 1 σ τ
+  simp only [Subst.liftn_one] at h
+  exact h
+
+end Terminator
+
+/-- Substitute the free labels in this basic block -/
+def Block.lsubst (σ : Terminator.Subst φ) (β : Block φ) : Block φ where
+  body := β.body
+  terminator := β.terminator.lsubst (σ.vliftn β.body.num_defs)
+
+/-- Substitute the free labels in this region -/
+def BBRegion.lsubst (σ : Terminator.Subst φ) : BBRegion φ → BBRegion φ
+  | cfg β n f => cfg (β.lsubst (σ.liftn n)) n
+    (λ i => (f i).lsubst ((σ.liftn n).vliftn (β.body.num_defs + 1)))
+
+/-- Substitute the free labels in this control-flow graph -/
+def BBCFG.lsubst (σ : Terminator.Subst φ) (cfg : BBCFG φ) : BBCFG φ where
+  length := cfg.length
+  targets := λi => (cfg.targets i).lsubst σ
+
+/-- Substitute the free labels in this region -/
+def TRegion.lsubst (σ : Terminator.Subst φ) : TRegion φ → TRegion φ
+  | let1 e t => let1 e (t.lsubst σ.vlift)
+  | let2 e t => let2 e (t.lsubst (σ.vliftn 2))
+  | cfg β n f => cfg (β.lsubst (σ.liftn n)) n (λ i => (f i).lsubst (σ.liftn n).vlift)
+
+/-- Substitute the free labels in this control-flow graph -/
+def TCFG.lsubst (σ : Terminator.Subst φ) (cfg : TCFG φ) : TCFG φ where
+  length := cfg.length
+  targets := λi => (cfg.targets i).lsubst σ
diff --git a/DeBruijnSSA/BinSyntax/Typing/Region/Basic.lean b/DeBruijnSSA/BinSyntax/Typing/Region/Basic.lean
index 3634392..77b7bf3 100644
--- a/DeBruijnSSA/BinSyntax/Typing/Region/Basic.lean
+++ b/DeBruijnSSA/BinSyntax/Typing/Region/Basic.lean
@@ -12,7 +12,7 @@ namespace BinSyntax
 
 section Basic
 
-variable [Φ: EffInstSet φ (Ty α) ε] [PartialOrder α] [PartialOrder ε] [Bot ε]
+variable [Φ: EffInstSet φ (Ty α) ε] [PartialOrder α] [PartialOrder ε]
 
 theorem Ctx.Wkn.toFinWk_id {Γ Δ : Ctx α ε} {L L' R S : LCtx α} {ρ : Fin R.length → Fin S.length}
   (hρ : (R ++ L).Wkn (S ++ L') (Fin.toNatWk ρ)) (i : Fin R.length)
@@ -21,6 +21,8 @@ theorem Ctx.Wkn.toFinWk_id {Γ Δ : Ctx α ε} {L L' R S : LCtx α} {ρ : Fin R.
   simp only [Fin.getElem_fin, lift_id_iff, ge_iff_le, Prod.mk_le_mk, le_refl, and_true, h]
   exact hρ.toFinWk_append i
 
+variable [Bot ε]
+
 namespace Region
 
 inductive WfD : Ctx α ε → Region φ → LCtx α → Type _