diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Completeness.lean b/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Completeness.lean
index 069f2a6..21e4f16 100644
--- a/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Completeness.lean
+++ b/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Completeness.lean
@@ -36,7 +36,7 @@ theorem Eqv.packed_let1_den {Γ : Ctx α ε} {R : LCtx α}
   conv =>
     rhs
     rw [let1_pair, let1_pair]
-    simp only [let1_beta, Nat.liftnWk, Nat.ofNat_pos, ↓reduceIte, zero_add,
+    simp [let1_beta, Nat.liftnWk, ↓reduceIte, zero_add,
     Term.Eqv.subst_liftn₂_var_one, Term.Eqv.var_succ_subst0, Term.Eqv.var0_subst0, List.length_cons,
     ↓dreduceIte, Nat.reduceAdd, Set.mem_setOf_eq, Ctx.InS.coe_lift, Ctx.InS.coe_wk2,
     Nat.liftWk_succ, id_eq, Nat.reduceSub, Nat.succ_eq_add_one, Fin.zero_eta, List.get_eq_getElem,
@@ -61,9 +61,9 @@ theorem Eqv.packed_let1_den {Γ : Ctx α ε} {R : LCtx α}
     apply Term.Eqv.eq_of_term_eq
     simp only [Term.InS.coe_subst, Term.InS.coe_subst0, Term.InS.coe_pi_n, Term.pi_n, Term.subst_pn,
       Term.wk_pn, Term.InS.coe_wk,
-      Term.InS.coe_pair, Term.InS.coe_var, List.length_cons, Term.Subst.liftn, Nat.ofNat_pos,
-      ↓reduceIte, Ctx.InS.lift_wk0, Term.Subst.InS.coe_comp, Term.Subst.InS.coe_lift, Ctx.InS.coe_wk1,
-      Nat.liftnWk]
+      Term.InS.coe_pair, Term.InS.coe_var, List.length_cons, Term.Subst.liftn,
+      ↓reduceIte, Ctx.InS.lift_wk0, Term.Subst.InS.coe_comp, Term.Subst.InS.coe_lift,
+      Ctx.InS.coe_wk1, Nat.liftnWk]
     rfl
 
 theorem Eqv.packed_let2_den {Γ : Ctx α ε} {R : LCtx α}
@@ -91,7 +91,7 @@ theorem Eqv.packed_let2_den {Γ : Ctx α ε} {R : LCtx α}
     Term.Eqv.var_succ_subst0, Term.Eqv.wk0_var, zero_add, Term.Eqv.subst_lift_var_zero,
     Term.Eqv.var0_subst0, Nat.reduceAdd, Nat.liftWk_succ, Nat.succ_eq_add_one, Term.Eqv.wk_res_self,
     assoc_inv, ret_seq, vwk1_let2, Term.Eqv.wk1_var0, vwk3, vwk_let2, Term.Eqv.wk_var,
-    Set.mem_setOf_eq, Ctx.InS.coe_wk3, Nat.liftnWk, Nat.ofNat_pos, ↓reduceIte, vwk_br,
+    Set.mem_setOf_eq, Ctx.InS.coe_wk3, Nat.liftnWk, ↓reduceIte, vwk_br,
     Term.Eqv.wk_pair, Ctx.InS.coe_liftn₂, Nat.reduceLT, Nat.reduceSub, Nat.one_lt_ofNat,
     vsubst_let2, ge_iff_le, le_refl, Term.Eqv.subst_liftn₂_var_zero,
     Term.Eqv.subst_liftn₂_var_add_2, Term.Eqv.subst_liftn₂_var_one, let2_pair, let1_beta,
@@ -103,7 +103,7 @@ theorem Eqv.packed_let2_den {Γ : Ctx α ε} {R : LCtx α}
     apply Term.Eqv.eq_of_term_eq
     simp only [List.get_eq_getElem, List.length_cons, Set.mem_setOf_eq, Term.Subst.InS.get_comp,
       Term.InS.coe_subst, Ctx.InS.coe_toSubst, Ctx.InS.coe_wk2, Term.InS.coe_subst0,
-      Term.InS.coe_pair, Term.InS.coe_var, Term.Subst.liftn, Nat.ofNat_pos, ↓reduceIte,
+      Term.InS.coe_pair, Term.InS.coe_var, Term.Subst.liftn, ↓reduceIte,
       Term.subst_fromWk, Term.Subst.InS.unpack, Term.Subst.InS.get, Term.Subst.InS.coe_comp,
       Term.Subst.pi_n, Term.Subst.comp, Term.pi_n, Term.subst_pn, Term.wk_pn]
     rfl
@@ -133,7 +133,7 @@ theorem Eqv.packed_case_den {Γ : Ctx α ε} {R : LCtx α}
   · rw [distl_inv, ret_seq]
     simp only [let1_beta, vwk1_let2, Term.Eqv.wk1_var0, List.length_cons, Fin.zero_eta,
       List.get_eq_getElem, Fin.val_zero, List.getElem_cons_zero, vwk3, vwk_case, Term.Eqv.wk_var,
-      Set.mem_setOf_eq, Ctx.InS.coe_wk3, Nat.liftnWk, Nat.ofNat_pos, ↓reduceIte, vwk_br,
+      Set.mem_setOf_eq, Ctx.InS.coe_wk3, Nat.liftnWk, ↓reduceIte, vwk_br,
       Term.Eqv.wk_inl, Term.Eqv.wk_pair, Ctx.InS.coe_lift, Nat.liftWk_succ, Nat.one_lt_ofNat,
       Nat.reduceAdd, Nat.liftWk_zero, Term.Eqv.wk_inr, vsubst_let2, Term.Eqv.var0_subst0,
       Term.Eqv.wk_res_self, vsubst_case, ge_iff_le, le_refl, Term.Eqv.subst_liftn₂_var_zero,
@@ -186,7 +186,7 @@ theorem Eqv.unpacked_app_out_eq_left_exit' {Γ : Ctx α ε} {R L : LCtx α}
     left_exit, List.getElem_cons_succ, vwk1_case, wk1_var0, List.length_cons, Fin.zero_eta, vwk2_br,
     wk2_var0, vwk1_br, wk1_pack_app, Subst.Eqv.get_comp, get_alpha0, List.length_nil, Fin.val_succ,
     Fin.cases_zero, lsubst_br, Subst.Eqv.get_vlift, Subst.Eqv.get_toSubstE, Set.mem_setOf_eq,
-    Fin.coe_fin_one, LCtx.InS.coe_wk1, Nat.liftWk_zero, Nat.reduceAdd, zero_add, vwk_id_eq,
+    Fin.val_eq_zero, LCtx.InS.coe_wk1, Nat.liftWk_zero, Nat.reduceAdd, zero_add, vwk_id_eq,
     vsubst_case, var0_subst0, wk_res_self, vsubst_br, subst_lift_var_zero, Nat.add_zero,
     Nat.zero_eq]
   rfl
@@ -230,7 +230,7 @@ theorem Eqv.packed_cfg_den {Γ : Ctx α ε} {L R : LCtx α} {β : Eqv φ Γ (R +
       let2_seq, vwk2_inj_r, vwk1_br, wk1_pack_app, Term.Eqv.distl_inv, vwk1_pi_r, vsubst_lift_seq,
       vsubst_lift_pi_r, vsubst_lift_inj_l, wk1_let2, wk1_nil, ← Ctx.InS.lift_lift, Ctx.InS.lift_wk1,
       wk_lift_coprod, wk_inl, wk_pair, wk_var, Set.mem_setOf_eq, Ctx.InS.coe_lift, Ctx.InS.coe_wk2,
-      Nat.liftWk_succ, Nat.liftnWk, Nat.ofNat_pos, ↓reduceIte, zero_add, wk_lift_nil, wk_inr]
+      Nat.liftWk_succ, Nat.liftnWk, ↓reduceIte, zero_add, wk_lift_nil, wk_inr]
     congr 1
     conv => rhs; rw [<-ret, case_let2, seq_assoc]; rhs; rw [ret_seq]
     simp only [vwk2, ← Ctx.InS.lift_wk1, vwk_lift_seq, vwk_case, wk_var, Set.mem_setOf_eq,
@@ -242,7 +242,7 @@ theorem Eqv.packed_cfg_den {Γ : Ctx α ε} {L R : LCtx α} {β : Eqv φ Γ (R +
       vsubst_case, subst_lift_nil, subst_inl, subst_pair, subst_lift_var_succ, subst_lift_var_zero,
       wk0_var, vsubst_lift_seq, vsubst_lift_pi_r, vsubst_lift_inj_l, vsubst_lift_inj_r, subst_inr,
       let2_pair, let1_beta, var_succ_subst0, var0_subst0, List.length_cons, Nat.add_zero,
-      Nat.zero_eq, Nat.succ_eq_add_one, Ctx.InS.coe_wk2, Nat.liftnWk, Nat.ofNat_pos, ↓dreduceIte,
+      Nat.zero_eq, Nat.succ_eq_add_one, Ctx.InS.coe_wk2, Nat.liftnWk, ↓dreduceIte,
       Nat.reduceSub, Fin.zero_eta, List.get_eq_getElem, Fin.val_zero, List.getElem_cons_zero,
       wk_res_self, nil_vwk_lift]
     simp only [packed_out_unpacked_app_out_ret_seq, LCtx.pack.eq_1, seq_assoc, case_inl, case_inr]
diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Product.lean b/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Product.lean
index ea00c44..0638dfa 100644
--- a/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Product.lean
+++ b/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Product.lean
@@ -120,10 +120,10 @@ def Eqv.ret_seq_rtimes {tyLeft tyIn tyOut : Ty α} {Γ : Ctx α ε} {L : LCtx α
     ret (pair (var 1 (by simp)) (var 0 (by simp)))) := by
     rw [ret_seq, rtimes, vwk1]
     simp only [vwk_let2, wk_var, Set.mem_setOf_eq, Ctx.InS.coe_wk1, Nat.liftWk_zero, vwk_liftn₂_seq,
-      vwk_ret, wk_pair, Ctx.InS.coe_liftn₂, Nat.liftnWk, Nat.one_lt_ofNat, ↓reduceIte,
-      Nat.ofNat_pos, vsubst_let2, var0_subst0, List.length_cons, id_eq, Fin.zero_eta,
-      List.get_eq_getElem, Fin.val_zero, List.getElem_cons_zero, wk_res_self, vsubst_liftn₂_seq,
-      vsubst_br, subst_pair, subst_liftn₂_var_one, ge_iff_le, le_refl, subst_liftn₂_var_zero]
+      vwk_br, wk_pair, Ctx.InS.coe_liftn₂, Nat.liftnWk, Nat.one_lt_ofNat, ↓reduceIte, zero_lt_two,
+      vsubst_let2, var0_subst0, List.length_cons, id_eq, Fin.zero_eta, List.get_eq_getElem,
+      Fin.val_zero, List.getElem_cons_zero, wk_res_self, vsubst_liftn₂_seq, vsubst_br, subst_pair,
+      subst_liftn₂_var_one, ge_iff_le, le_refl, subst_liftn₂_var_zero]
     congr
     induction r using Quotient.inductionOn
     induction e using Quotient.inductionOn
@@ -288,14 +288,7 @@ theorem Eqv.vsubst_lift_pi_r {Γ Δ : Ctx α ε} {L : LCtx α} {ρ : Term.Subst.
 theorem Eqv.ret_pair_pi_r {Γ : Ctx α ε} {L : LCtx α} {A B : Ty α}
   {a : Term.Eqv φ ((X, ⊥)::Γ) (A, ⊥)} {b : Term.Eqv φ ((X, ⊥)::Γ) (B, ⊥)}
   : ret (targets := L) (a.pair b) ;; pi_r = ret b
-  := by
-  simp only [pi_r, ret_seq, vwk1, vwk_let2, wk_var, Set.mem_setOf_eq, Ctx.InS.coe_wk1,
-    Nat.liftWk_zero, vwk_ret, Ctx.InS.coe_liftn₂, Nat.liftnWk, Nat.ofNat_pos, ↓reduceIte,
-    vsubst_let2, var0_subst0, List.length_cons, id_eq, Fin.zero_eta, List.get_eq_getElem,
-    Fin.val_zero, List.getElem_cons_zero, wk_res_self, vsubst_br, ge_iff_le, le_refl,
-    subst_liftn₂_var_zero, let2_pair, let1_beta, ret]
-  congr
-  exact subst0_wk0
+  := by simp [pi_r, ret_seq, vwk1, Nat.liftnWk, vsubst_let2, let2_pair, let1_beta]
 
 @[simp]
 theorem Eqv.Pure.pi_r {Γ : Ctx α ε} {L : LCtx α}
@@ -314,16 +307,8 @@ theorem Eqv.lunit_pi_r {ty : Ty α} {Γ : Ctx α ε} {L : LCtx α}
 
 theorem Eqv.ret_pair_braid {Γ : Ctx α ε} {L : LCtx α} {A B : Ty α}
   {a : Term.Eqv φ ((X, ⊥)::Γ) (A, ⊥)} {b : Term.Eqv φ ((X, ⊥)::Γ) (B, ⊥)}
-  : ret (targets := L) (a.pair b) ;; braid = ret (pair b a) := by
-  simp only [braid, ret_seq, vwk1, vwk_let2, wk_var, Set.mem_setOf_eq, Ctx.InS.coe_wk1,
-    Nat.liftWk_zero, vwk_ret, wk_pair, Ctx.InS.coe_liftn₂, Nat.liftnWk, Nat.ofNat_pos, ↓reduceIte,
-    Nat.one_lt_ofNat, vsubst_let2, var0_subst0, List.length_cons, id_eq, Fin.zero_eta,
-    List.get_eq_getElem, Fin.val_zero, List.getElem_cons_zero, wk_res_self, vsubst_br, subst_pair,
-    ge_iff_le, le_refl, subst_liftn₂_var_zero, subst_liftn₂_var_one, let2_pair, let1_beta,
-    var_succ_subst0, ↓dreduceIte, Nat.reduceSub, Nat.reduceAdd]
-  simp only [ret]
-  congr
-  exact subst0_wk0
+  : ret (targets := L) (a.pair b) ;; braid = ret (pair b a)
+  := by simp [braid, ret_seq, vwk1, Nat.liftnWk, subst_pair, let2_pair, let1_beta, subst0_wk0]
 
 theorem Eqv.ltimes_def' {tyIn tyOut tyRight : Ty α} {Γ : Ctx α ε} {L : LCtx α}
   {r : Eqv φ (⟨tyIn, ⊥⟩::Γ) (tyOut::L)}
@@ -668,7 +653,7 @@ theorem Eqv.assoc_right_nat {A B C C' : Ty α} {Γ : Ctx α ε} {L : LCtx α}
   induction r using Quotient.inductionOn
   apply Eqv.eq_of_reg_eq
   simp only [Set.mem_setOf_eq, InS.vwk_br, Term.InS.wk_pair, Term.InS.wk_var, Ctx.InS.coe_swap02,
-    Nat.ofNat_pos, Nat.swap0_lt, Nat.swap0_0, Nat.one_lt_ofNat, Ctx.InS.coe_wk1, Nat.liftWk_succ,
+    zero_lt_two, Nat.swap0_lt, Nat.swap0_0, Nat.one_lt_ofNat, Ctx.InS.coe_wk1, Nat.liftWk_succ,
     Nat.succ_eq_add_one, Nat.reduceAdd, zero_add, Nat.liftWk_zero, InS.coe_vwk, InS.coe_lsubst,
     InS.coe_alpha0, InS.coe_br, Term.InS.coe_pair, Term.InS.coe_var, Region.vwk_lsubst,
     InS.coe_vsubst, Term.InS.coe_subst0, Term.Subst.InS.coe_liftn₂, Region.vsubst_lsubst]
diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Region/LSubst.lean b/DeBruijnSSA/BinSyntax/Rewrite/Region/LSubst.lean
index bf9b8f5..b46e097 100644
--- a/DeBruijnSSA/BinSyntax/Rewrite/Region/LSubst.lean
+++ b/DeBruijnSSA/BinSyntax/Rewrite/Region/LSubst.lean
@@ -48,22 +48,22 @@ theorem Subst.InS.liftn_append_congr {Γ : Ctx α ε} {L K J : LCtx α}
         by have h'' := i.prop; simp only [List.length_append] at h''; omega
       ⟩) using 1
     congr 3
-    rw [List.getElem_append_right _ _ h']
+    rw [List.getElem_append_right (le_of_not_lt h')]
     rfl
     congr 4
-    rw [List.getElem_append_right _ _ h']
+    rw [List.getElem_append_right (le_of_not_lt h')]
     rfl
     congr 1
     funext r
     simp only [Set.mem_setOf_eq, List.get_eq_getElem]
     congr 3
-    rw [List.getElem_append_right _ _ h']
+    rw [List.getElem_append_right (le_of_not_lt h')]
     apply proof_irrel_heq
     congr 1
     funext r
     simp only [Set.mem_setOf_eq, List.get_eq_getElem]
     congr 3
-    rw [List.getElem_append_right _ _ h']
+    rw [List.getElem_append_right (le_of_not_lt h')]
     apply proof_irrel_heq
 
 theorem Subst.InS.slift_congr {Γ : Ctx α ε} {L K : LCtx α}
@@ -589,9 +589,7 @@ theorem Eqv.cfgSubst'_get {Γ : Ctx α ε} {L : LCtx α}
           simp only [List.get_eq_getElem]
           rw [List.getElem_append_right]
           apply LCtx.Trg.of_getElem
-          assumption
-          have hi : i < R.length + L.length := List.length_append _ _ ▸ i.prop;
-          omega
+          exact (le_of_not_lt h)
         )
   := by
   induction G using Eqv.choiceInduction
@@ -609,8 +607,6 @@ theorem Eqv.cfgSubst'_get_ge  {Γ : Ctx α ε} {L : LCtx α}
       rw [List.getElem_append_right]
       apply LCtx.Trg.of_getElem
       omega
-      have hi : i < R.length + L.length := List.length_append _ _ ▸ i.prop;
-      omega
     )
   := by rw [Eqv.cfgSubst'_get, dite_cond_eq_false]; simp [h]
 
@@ -705,9 +701,7 @@ theorem Eqv.cfgSubst_get' {Γ : Ctx α ε} {L : LCtx α}
           simp only [List.get_eq_getElem]
           rw [List.getElem_append_right]
           apply LCtx.Trg.of_getElem
-          assumption
-          have hi : i < R.length + L.length := List.length_append _ _ ▸ i.prop;
-          omega
+          exact (le_of_not_lt h)
         )
   := by rw [cfgSubst_eq_cfgSubst', cfgSubst'_get]
 
@@ -719,8 +713,6 @@ theorem Eqv.cfgSubst_get_ge  {Γ : Ctx α ε} {L : LCtx α}
       rw [List.getElem_append_right]
       apply LCtx.Trg.of_getElem
       omega
-      have hi : i < R.length + L.length := List.length_append _ _ ▸ i.prop;
-      omega
     )
   := by rw [Eqv.cfgSubst_get', dite_cond_eq_false]; simp [h]
 
diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Region/Structural/Distrib.lean b/DeBruijnSSA/BinSyntax/Rewrite/Region/Structural/Distrib.lean
index 8cf1d6f..2eb51a8 100644
--- a/DeBruijnSSA/BinSyntax/Rewrite/Region/Structural/Distrib.lean
+++ b/DeBruijnSSA/BinSyntax/Rewrite/Region/Structural/Distrib.lean
@@ -119,12 +119,12 @@ theorem Eqv.packed_out_binary_rtimes {Γ : Ctx α ε} {L : LCtx α}
   congr 2
   simp only [distl_inv_eq_ret, pi_r, ret_seq, vwk1_sum, vwk1_let2, wk1_var0, List.length_cons,
     Fin.zero_eta, List.get_eq_getElem, Fin.val_zero, List.getElem_cons_zero, vwk3, vwk_br, wk_var,
-    Set.mem_setOf_eq, Ctx.InS.coe_wk3, Nat.liftnWk, Nat.ofNat_pos, ↓reduceIte,
+    Set.mem_setOf_eq, Ctx.InS.coe_wk3, Nat.liftnWk, ↓reduceIte,
     nil_vwk1]
   simp only [sum, coprod, nil_seq, vwk1_inj_l, vwk1_seq, vwk1_br, wk1_pair, wk1_var_succ, zero_add,
     wk1_var0, List.length_cons, Fin.zero_eta, List.get_eq_getElem, Fin.val_zero,
     List.getElem_cons_zero, vwk1_inj_r, vwk1_let2, vwk3, vwk_br, wk_var, Set.mem_setOf_eq,
-    Ctx.InS.coe_wk3, Nat.liftnWk, Nat.ofNat_pos, ↓reduceIte, vsubst_case, var0_subst0, wk_res_self,
+    Ctx.InS.coe_wk3, Nat.liftnWk, ↓reduceIte, vsubst_case, var0_subst0, wk_res_self,
     vsubst_lift_seq, vsubst_let2, subst_lift_var_zero, vsubst_br, ge_iff_le, le_refl,
     subst_liftn₂_var_zero, vsubst_lift_inj_l, vsubst_lift_inj_r, vwk1_case, wk1_distl_inv, vwk2, ←
     Ctx.InS.lift_wk1, vwk_lift_seq, vwk_let2, Ctx.InS.coe_lift, Ctx.InS.coe_wk1, Nat.liftWk_zero,
diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Region/Structural/Elgot.lean b/DeBruijnSSA/BinSyntax/Rewrite/Region/Structural/Elgot.lean
index 413795b..e7f62ad 100644
--- a/DeBruijnSSA/BinSyntax/Rewrite/Region/Structural/Elgot.lean
+++ b/DeBruijnSSA/BinSyntax/Rewrite/Region/Structural/Elgot.lean
@@ -59,7 +59,7 @@ theorem Eqv.packed_out_sum_coprod {β : Eqv φ ((X, ⊥)::Γ) [A, B]}
         Term.Eqv.wk2_var0, vwk2_quot, sum, inj_r, nil_seq, Term.Eqv.wk1_inr, Term.Eqv.wk2_inr,
         Subst.Eqv.get_comp, Subst.Eqv.pack_get, Term.Eqv.inj_n, Term.Eqv.nil, Fin.val_succ,
         List.getElem_cons_succ, List.length_nil, Fin.cases_zero, lsubst_br, Fin.isValue,
-        Subst.Eqv.get_vlift, get_alpha0, Fin.coe_fin_one, zero_add, lsubst_case, vwk_id_eq,
+        Subst.Eqv.get_vlift, get_alpha0, Fin.val_eq_zero, zero_add, lsubst_case, vwk_id_eq,
         vsubst_case, Term.Eqv.var0_subst0, Term.Eqv.wk_res_self, vsubst_br,
         Term.Eqv.subst_lift_var_zero, case_inr, let1_beta]
       rfl
@@ -83,8 +83,8 @@ theorem Eqv.packed_out_sum_coprod {β : Eqv φ ((X, ⊥)::Γ) [A, B]}
       simp only [vwk2, Term.Eqv.wk1_abort, Term.Eqv.wk1_var0, List.length_cons, Fin.zero_eta,
         List.get_eq_getElem, Fin.val_zero, List.getElem_cons_zero, lsubst_br, List.length_singleton,
         Nat.reduceAdd, Fin.isValue, Subst.Eqv.get_vlift, get_alpha0, Fin.val_succ,
-        List.getElem_cons_succ, Fin.coe_fin_one, zero_add, Fin.cases_zero, vwk1_case, vwk_br,
-        Term.Eqv.wk_var, Set.mem_setOf_eq, Ctx.InS.coe_wk2, Nat.liftnWk, Nat.ofNat_pos, ↓reduceIte,
+        List.getElem_cons_succ, Fin.val_eq_zero, zero_add, Fin.cases_zero, vwk1_case, vwk_br,
+        Term.Eqv.wk_var, Set.mem_setOf_eq, Ctx.InS.coe_wk2, Nat.liftnWk, ↓reduceIte,
         vwk_id_eq, vsubst_case, Term.Eqv.var0_subst0, Term.Eqv.wk_res_self, vsubst_br,
         Term.Eqv.subst_lift_var_zero, vwk_case, Ctx.InS.coe_lift, Nat.liftWk_zero]
       rw [<-vwk2, <-vwk2, nil_vwk2, nil_vwk2, <-ret_var_zero]
diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Region/Structural/Sum.lean b/DeBruijnSSA/BinSyntax/Rewrite/Region/Structural/Sum.lean
index 6580f94..1d8ec21 100644
--- a/DeBruijnSSA/BinSyntax/Rewrite/Region/Structural/Sum.lean
+++ b/DeBruijnSSA/BinSyntax/Rewrite/Region/Structural/Sum.lean
@@ -359,7 +359,7 @@ theorem Subst.Eqv.pack_comp_unpack {Γ : Ctx α ε} {R : LCtx α}
   : Subst.Eqv.pack.comp Subst.Eqv.unpack = Subst.Eqv.id (φ := φ) (Γ := Γ) (L := [R.pack]) := by
   ext ℓ
   induction ℓ using Fin.elim1
-  simp only [unpack, get_comp, vlift_pack, Eqv.csubst_get, Eqv.cast_rfl, get_id, Fin.coe_fin_one]
+  simp only [unpack, get_comp, vlift_pack, Eqv.csubst_get, Eqv.cast_rfl, get_id, Fin.val_eq_zero]
   rw [<-Eqv.packed_out, Eqv.packed_out_unpack]
   rfl
 
@@ -455,7 +455,7 @@ theorem Eqv.lsubst_pack_append_vlift_unpack {Γ : Ctx α ε} {L R : LCtx α}
         Term.Eqv.wk1_var0, vwk_id_eq, vsubst_br, Term.Eqv.var0_subst0, Term.Eqv.wk_res_self,
         Term.Eqv.inj_r, vwk2, lwk_id_eq_lwk, Set.mem_setOf_eq, lwk_case, lwk_quot, vwk1_case,
         LCtx.pack.eq_2, vwk_quot, vwk_case, Term.Eqv.wk_var, Ctx.InS.coe_wk2, Nat.liftnWk,
-        Nat.ofNat_pos, ↓reduceIte, let1_beta, vsubst_case, Term.Eqv.subst_lift_nil,
+        zero_lt_two, ↓reduceIte, let1_beta, vsubst_case, Term.Eqv.subst_lift_nil,
         Term.Eqv.subst_lift_var_zero, case_inr, Nat.add_zero, Nat.zero_eq, ↓dreduceIte,
         Nat.reduceSub, Nat.succ_eq_add_one, Nat.reduceAdd]
       apply eq_of_reg_eq
@@ -660,7 +660,7 @@ theorem Eqv.packed_out_binary_ret_seq  {Γ : Ctx α ε}
   | zero =>
     simp only [List.get_eq_getElem, List.length_cons, List.length_singleton, Nat.reduceAdd,
       Fin.val_zero, List.getElem_cons_zero, Subst.Eqv.get_comp, Subst.Eqv.vlift_pack, get_alpha0,
-      Fin.val_succ, List.getElem_cons_succ, Fin.coe_fin_one, zero_add, Term.Eqv.nil, Fin.cases_zero,
+      Fin.val_succ, List.getElem_cons_succ, Fin.val_eq_zero, zero_add, Term.Eqv.nil, Fin.cases_zero,
       lsubst_br, Fin.zero_eta, Fin.isValue, Subst.Eqv.pack_get, LCtx.pack.eq_2, LCtx.pack.eq_1,
       Term.Eqv.inj_n, List.length_nil, vwk_id_eq, vsubst_br, Term.Eqv.subst_inr,
       Term.Eqv.var0_subst0, Term.Eqv.wk_res_self, sum, coprod, nil_seq, inj_r, ret_seq, vwk1_br,
@@ -738,7 +738,7 @@ theorem Eqv.unpacked_app_out_seq {Γ : Ctx α ε} {R L : LCtx α}
   simp only [Fin.isValue, List.get_eq_getElem, List.length_singleton, Fin.val_zero,
     List.getElem_cons_zero, Subst.Eqv.get_comp, Subst.Eqv.vlift_unpack_app_out, get_alpha0,
     List.length_nil, Fin.val_succ, List.getElem_cons_succ, Fin.cases_zero, Subst.Eqv.get_toSubstE,
-    Set.mem_setOf_eq, Fin.coe_fin_one, LCtx.InS.coe_wk1, Nat.liftWk_zero, lsubst_br,
+    Set.mem_setOf_eq, Fin.val_eq_zero, LCtx.InS.coe_wk1, Nat.liftWk_zero, lsubst_br,
     List.length_cons, Nat.reduceAdd, Fin.zero_eta, Subst.Eqv.get_vlift, zero_add, vwk_id_eq,
     vsubst0_var0_vwk1]
   rw [vwk1_unpacked_app_out]; rfl
diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Term/Structural/Product.lean b/DeBruijnSSA/BinSyntax/Rewrite/Term/Structural/Product.lean
index 8ecc30a..c6eb516 100644
--- a/DeBruijnSSA/BinSyntax/Rewrite/Term/Structural/Product.lean
+++ b/DeBruijnSSA/BinSyntax/Rewrite/Term/Structural/Product.lean
@@ -278,7 +278,7 @@ theorem Subst.Eqv.unpack_comp_packSE {Γ : Ctx α ε} (h : Γ.Pure)
   : unpack.comp h.packSE = Subst.Eqv.id (φ := φ) := by
   ext k; cases k using Fin.elim1
   simp only [Fin.isValue, List.get_eq_getElem, List.length_singleton, Fin.val_zero,
-    List.getElem_cons_zero, get_comp, get_packSE_zero, get_id, Fin.coe_fin_one]
+    List.getElem_cons_zero, get_comp, get_packSE_zero, get_id, Fin.val_eq_zero]
   exact Eqv.packed_packE
 
 -- theorem Eqv.pi_n_eq_pi_n' {Γ Δ : Ctx α ε} (i : Fin Γ.length) :
diff --git a/DeBruijnSSA/BinSyntax/Syntax/Definitions.lean b/DeBruijnSSA/BinSyntax/Syntax/Definitions.lean
index a796afa..4bf494f 100644
--- a/DeBruijnSSA/BinSyntax/Syntax/Definitions.lean
+++ b/DeBruijnSSA/BinSyntax/Syntax/Definitions.lean
@@ -219,7 +219,7 @@ theorem TRegion.toRegion_inj {t₁ t₂ : TRegion φ} : t₁.toRegion = t₂.toR
     simp only [toRegion, Region.cfg.injEq, Terminator.toRegion_inj, cfg.injEq, and_congr_right_iff]
     intro hβ hn
     cases hβ; cases hn
-    simp only [heq_eq_eq, Function.funext_iff, *]
+    simp only [heq_eq_eq, funext_iff, *]
   all_goals simp [Terminator.toRegion_inj, *]
 
 theorem TRegion.toRegion_injective : Function.Injective (@TRegion.toRegion φ)
diff --git a/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Region/Cong.lean b/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Region/Cong.lean
index 8396b35..8975064 100644
--- a/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Region/Cong.lean
+++ b/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Region/Cong.lean
@@ -1,6 +1,5 @@
 import Mathlib.Combinatorics.Quiver.Path
 import Mathlib.Combinatorics.Quiver.Symmetric
-import Mathlib.CategoryTheory.PathCategory
 import Mathlib.Algebra.Order.BigOperators.Group.Finset
 
 import Discretion.Correspondence.Definitions
diff --git a/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Region/Equiv.lean b/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Region/Equiv.lean
index 8cdebdb..047394d 100644
--- a/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Region/Equiv.lean
+++ b/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Region/Equiv.lean
@@ -1,6 +1,5 @@
 import Mathlib.Combinatorics.Quiver.Path
 import Mathlib.Combinatorics.Quiver.Symmetric
-import Mathlib.CategoryTheory.PathCategory
 import Mathlib.Algebra.Order.BigOperators.Group.Finset
 
 import Discretion.Correspondence.Definitions
diff --git a/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Region/Reduce.lean b/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Region/Reduce.lean
index 109302c..dbd525d 100644
--- a/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Region/Reduce.lean
+++ b/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Region/Reduce.lean
@@ -1,6 +1,5 @@
 import Mathlib.Combinatorics.Quiver.Path
 import Mathlib.Combinatorics.Quiver.Symmetric
-import Mathlib.CategoryTheory.PathCategory
 import Mathlib.Algebra.Order.BigOperators.Group.Finset
 
 import Discretion.Correspondence.Definitions
diff --git a/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Region/Rewrite.lean b/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Region/Rewrite.lean
index b416ad3..13b6b31 100644
--- a/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Region/Rewrite.lean
+++ b/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Region/Rewrite.lean
@@ -1,6 +1,5 @@
 import Mathlib.Combinatorics.Quiver.Path
 import Mathlib.Combinatorics.Quiver.Symmetric
-import Mathlib.CategoryTheory.PathCategory
 import Mathlib.Algebra.Order.BigOperators.Group.Finset
 
 import Discretion.Correspondence.Definitions
diff --git a/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Region/Step.lean b/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Region/Step.lean
index bd00cef..aa97489 100644
--- a/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Region/Step.lean
+++ b/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Region/Step.lean
@@ -1,6 +1,5 @@
 import Mathlib.Combinatorics.Quiver.Path
 import Mathlib.Combinatorics.Quiver.Symmetric
-import Mathlib.CategoryTheory.PathCategory
 import Mathlib.Algebra.Order.BigOperators.Group.Finset
 
 import Discretion.Correspondence.Definitions
diff --git a/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Term/Cong.lean b/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Term/Cong.lean
index b896635..528625d 100644
--- a/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Term/Cong.lean
+++ b/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Term/Cong.lean
@@ -1,6 +1,5 @@
 import Mathlib.Combinatorics.Quiver.Path
 import Mathlib.Combinatorics.Quiver.Symmetric
-import Mathlib.CategoryTheory.PathCategory
 import Mathlib.Algebra.Order.BigOperators.Group.Finset
 
 import Discretion.Correspondence.Definitions
diff --git a/DeBruijnSSA/BinSyntax/Syntax/Subst/Region.lean b/DeBruijnSSA/BinSyntax/Syntax/Subst/Region.lean
index f48139a..f188486 100644
--- a/DeBruijnSSA/BinSyntax/Syntax/Subst/Region.lean
+++ b/DeBruijnSSA/BinSyntax/Syntax/Subst/Region.lean
@@ -596,7 +596,8 @@ theorem vsubst_lift₃_vwk2 {ρ : Term.Subst φ} {r : Region φ}
   funext k; cases k using Nat.cases2 with
   | rest k =>
     simp_arith only [
-      Term.Subst.comp, Term.Subst.lift, Term.subst, Nat.liftnWk, Term.subst_fromWk, Term.wk_wk
+      Term.Subst.comp, Term.Subst.lift, Term.subst, Nat.liftnWk, Term.subst_fromWk, Term.wk_wk,
+      ↓reduceIte
     ]
     rfl
   | _ => rfl
diff --git a/DeBruijnSSA/BinSyntax/Typing/LCtx.lean b/DeBruijnSSA/BinSyntax/Typing/LCtx.lean
index e472117..1ec68bc 100644
--- a/DeBruijnSSA/BinSyntax/Typing/LCtx.lean
+++ b/DeBruijnSSA/BinSyntax/Typing/LCtx.lean
@@ -71,12 +71,8 @@ theorem getElem_shf_rest_add {R : LCtx α} {Y : Ty α} {L : LCtx α} {n}
     simp only [shf_rest, drop, List.cons_append, List.drop_succ_cons, List.drop_zero,
       List.length_cons, Nat.add_comm R.length 1, <-Nat.add_assoc]
     rw [List.getElem_append_right]
-    simp only [Nat.add_sub_cancel]
-    simp
-    omega
-    simp at hn
-    simp only [add_tsub_cancel_right, List.length_cons, add_lt_add_iff_right]
-    omega
+    · simp
+    · omega
 
 variable [Φ: EffInstSet φ (Ty α) ε] [PartialOrder α] [PartialOrder ε] [Bot ε]
 
@@ -244,10 +240,10 @@ theorem Wkn.toFinWk_append {L L' R S : LCtx α} {ρ : Fin R.length → Fin S.len
   (hρ : (R ++ L).Wkn (S ++ L') (Fin.toNatWk ρ)) (i : Fin R.length)
   : R[i] ≤ S[ρ i] := by
   have hρ := hρ i (Nat.lt_of_lt_of_le i.prop (by simp));
-  rw [List.getElem_append _ (by simp), Fin.toNatWk_coe] at hρ
+  rw [List.getElem_append _ (by rw [List.length_append]; omega), Fin.toNatWk_coe] at hρ
   have hρ := hρ.getElem
-  rw [List.getElem_append _ (by simp)] at hρ
-  simp [hρ]
+  rw [List.getElem_append _ (by rw [List.length_append]; omega)] at hρ
+  convert hρ <;> simp
 
 theorem Trg.head (h : A' ≤ A) (L : LCtx α) : Trg (A::L) 0 A' where
   length := by simp
@@ -275,7 +271,7 @@ theorem Trg.of_ge {n} {A : Ty α} (h : Trg (R ++ L) n A) (hn : R.length ≤ n) :
   (hn' ▸ h).of_add
 
 theorem Trg.of_lt {n} {A : Ty α} (h : Trg (L ++ R) n A) (hn : n < L.length) : Trg L n A
-  := ⟨hn, List.getElem_append _ hn ▸ h.getElem⟩
+  := ⟨hn, by convert h.getElem using 1; simp [List.getElem_append, hn]⟩
 
 theorem Trg.add {n} {A : Ty α} (h : Trg L n A) (R) : Trg (R ++ L) (n + R.length) A
   := by induction R with
@@ -286,7 +282,8 @@ theorem Trg.ge {n} {A : Ty α} (h : Trg L (n - R.length) A) (hn : R.length ≤ n
   := by convert (h.add R); simp [*]
 
 theorem Trg.extend {n} {A : Ty α} (h : Trg L n A) : Trg (L ++ R) n A
-  := ⟨Nat.lt_of_lt_of_le h.length (by simp), List.getElem_append _ h.length ▸ h.getElem⟩
+  := ⟨Nat.lt_of_lt_of_le h.length (by simp),
+      by convert h.getElem using 1; simp [List.getElem_append, h.length]⟩
 
 theorem Trg.add_iff {n} {A : Ty α} {R : LCtx α} : Trg (R ++ L) (n + R.length) A ↔ Trg L n A
   := ⟨λh => h.of_add, λh => h.add R⟩
diff --git a/DeBruijnSSA/BinSyntax/Typing/Region/Compose.lean b/DeBruijnSSA/BinSyntax/Typing/Region/Compose.lean
index 8314eb3..d769c72 100644
--- a/DeBruijnSSA/BinSyntax/Typing/Region/Compose.lean
+++ b/DeBruijnSSA/BinSyntax/Typing/Region/Compose.lean
@@ -375,7 +375,7 @@ def InS.cfgSubst {Γ : Ctx α ε} {L : LCtx α} (R : LCtx α)
   (G : ∀i : Fin R.length, InS φ ((R.get i, ⊥)::Γ) (R ++ L))
   : Subst.InS φ Γ (R ++ L) L := ⟨
     Region.cfgSubst R.length (λi => G i),
-    λℓ => Wf.cfg (hR := rfl)
+    λℓ => Wf.cfg _ _ (hR := rfl)
       (Wf.br ⟨ℓ.prop, by simp⟩ (Term.Wf.var Ctx.Var.shead))
       (λi => (G i).prop.vwk1)⟩
 
@@ -418,7 +418,7 @@ def InS.cfgSubst' {Γ : Ctx α ε} {L : LCtx α} (R : LCtx α)
     Region.cfgSubst' R.length (λi => G i),
     λℓ => if h : ℓ < R.length then by
         simp only [Region.cfgSubst', h, ↓reduceIte]
-        exact Wf.cfg (hR := rfl)
+        exact Wf.cfg _ _ (hR := rfl)
           (Wf.br ⟨ℓ.prop, by simp⟩ (Term.Wf.var Ctx.Var.shead))
           (λi => (G i).prop.vwk1)
       else by
@@ -427,11 +427,11 @@ def InS.cfgSubst' {Γ : Ctx α ε} {L : LCtx α} (R : LCtx α)
         constructor
         · simp only [List.get_eq_getElem]
           rw [List.getElem_append_right]
-          exact h
-        · rw [Nat.sub_lt_iff_lt_add (Nat.le_of_not_lt h)]
-          have h := ℓ.prop
-          simp at h
-          exact h
+          exact (le_of_not_lt h)
+        -- · rw [Nat.sub_lt_iff_lt_add (Nat.le_of_not_lt h)]
+        --   have h := ℓ.prop
+        --   simp at h
+        --   exact h
     ⟩
 
 @[simp]
@@ -446,7 +446,7 @@ theorem InS.get_cfgSubst' {Γ : Ctx α ε} {L : LCtx α} (R : LCtx α)
       InS.cfg R (InS.br ℓ (Term.InS.var 0 Ctx.Var.shead) (by simp)) (λi => (G i).vwk1)
     else InS.br (ℓ - R.length) (Term.InS.var 0 Ctx.Var.shead) ⟨
       by have hℓ := ℓ.prop; simp only [List.length_append] at hℓ; omega,
-      by rw [List.get_eq_getElem, List.getElem_append_right]; exact h⟩ := by
+      by rw [List.get_eq_getElem, List.getElem_append_right]; exact (le_of_not_lt h)⟩ := by
   ext
   simp only [List.get_eq_getElem, Set.mem_setOf_eq, Subst.InS.coe_get, coe_cfgSubst',
   Region.cfgSubst']
diff --git a/DeBruijnSSA/BinSyntax/Typing/Region/LSubst.lean b/DeBruijnSSA/BinSyntax/Typing/Region/LSubst.lean
index 51f5672..e415f0c 100644
--- a/DeBruijnSSA/BinSyntax/Typing/Region/LSubst.lean
+++ b/DeBruijnSSA/BinSyntax/Typing/Region/LSubst.lean
@@ -142,19 +142,18 @@ theorem Region.Subst.InS.coe_clip (σ : Region.Subst.InS φ Γ L K)
 theorem Region.Subst.Wf.extend_in (hσ : σ.Wf Γ L (K ++ R))
   : (σ.extend L.length K.length).Wf Γ (L ++ R) (K ++ R)
   := λi => by if h : i < L.length then
-    simp only [List.get_eq_getElem, extend_lt, h, List.getElem_append_left _ _ h]
+    simp only [List.get_eq_getElem, extend_lt, h, List.getElem_append_left h]
     exact (hσ ⟨i, h⟩)
   else
     have h' := i.prop
     simp only [List.length_append] at h'
     rw [
-      List.get_eq_getElem, List.getElem_append_right _ _ h,
+      List.get_eq_getElem, List.getElem_append_right (le_of_not_lt h),
       Region.Subst.extend_ge (Nat.ge_of_not_lt h)
     ]
     apply Wf.br _ (Term.Wf.var Ctx.Var.shead)
-    · omega
-    · rw [LCtx.Trg.ge_iff (by simp)]
-      simp
+    rw [LCtx.Trg.ge_iff (by simp)]
+    simp
 
 theorem Region.Subst.Wf.fromFCFG_append {Γ : Ctx α ε} {L K : LCtx α}
   {G : Fin L.length → Region φ} (hG : ∀i : Fin L.length, (G i).Wf (⟨L.get i, ⊥⟩::Γ) (K ++ R))
@@ -178,7 +177,6 @@ theorem Region.Subst.Wf.fromFCFG_append {Γ : Ctx α ε} {L K : LCtx α}
     · have hi' := i.prop;
       simp at hi';
       omega
-    · exact h
 
 theorem Region.Subst.Wf.fromFCFG_append' {Γ : Ctx α ε} {L K : LCtx α}
   {G : Fin n → Region φ}
diff --git a/lake-manifest.json b/lake-manifest.json
index 1fe59e7..bd53fe2 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,17 +5,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "bf12ff6041cbab6eba6b54d9467baed807bb2bfd",
+   "rev": "dc72dcdb8e97b3c56bd70f06f043ed2dee3258e6",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
-   "configFile": "lakefile.lean"},
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2c8ae451ce9ffc83554322b14437159c1a9703f9",
+   "rev": "1357f4f49450abb9dfd4783e38219f4ce84f9785",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "50aaaf78b7db5bd635c19c660d59ed31b9bc9b5a",
+   "rev": "9ac12945862fa39eab7795c2f79bb9aa0c8e332c",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -35,16 +35,16 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "eb08eee94098fe530ccd6d8751a86fe405473d4c",
+   "rev": "baa65c6339a56bd22b7292aa4511c54b3cc7a6af",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.42",
+   "inputRev": "v0.0.43",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
-   "scope": "",
+   "scope": "leanprover",
    "rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "fb7841a6f4fb389ec0e47dd4677844d49906af3c",
+   "rev": "9b4088ccf0f44ddd7b1132bb1348aef8cf481e12",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2ba60fa2c384a94735454db11a2d523612eaabff",
+   "rev": "7bedaed1ef024add1e171cc17706b012a9a37802",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "e336e27e0824583a3919ded9a6cb5870b198bbbb",
+   "rev": "9248301da2c228348b194c74be94b0e0b0bbbb2c",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "632e2ca5a9a34f2f541ebfaa91795816fd679370",
+   "rev": "bdab441c6e43d326b72b8d1ddc8c61b96054bdf3",
    "name": "discretion",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
diff --git a/lean-toolchain b/lean-toolchain
index 98556ba..eff86fd 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.12.0-rc1
+leanprover/lean4:v4.13.0-rc3