Version bump

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]

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]

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]
 

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,

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]

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

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) :

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 φ)

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

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

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

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

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

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