diff --git a/Plfl.lean b/Plfl.lean
index 0bb1613..ef26472 100644
--- a/Plfl.lean
+++ b/Plfl.lean
@@ -1,6 +1,5 @@
 module
 prelude
-public import Plfl.Init
 public import Plfl.Lambda
 public import Plfl.Lambda.Properties
 public import Plfl.DeBruijn
diff --git a/Plfl/DeBruijn.lean b/Plfl/DeBruijn.lean
index dfb235b..c50c6b0 100644
--- a/Plfl/DeBruijn.lean
+++ b/Plfl/DeBruijn.lean
@@ -2,7 +2,7 @@ module
 
 -- https://plfa.github.io/DeBruijn/
 
-import Plfl.Init
+import Plfl.Init.Tactics
 import Batteries.Tactic.Init
 import Mathlib.Data.Nat.Notation
 import Mathlib.Tactic.Basic
diff --git a/Plfl/Init.lean b/Plfl/Init/Decidable'.lean
similarity index 61%
rename from Plfl/Init.lean
rename to Plfl/Init/Decidable'.lean
index e35a104..8e744c4 100644
--- a/Plfl/Init.lean
+++ b/Plfl/Init/Decidable'.lean
@@ -5,12 +5,6 @@ public import Mathlib.Logic.IsEmpty.Basic
 
 @[expose] public section
 
-/--
-`is_empty` converts `IsEmpty α` to `α → False`.
--/
-syntax "is_empty" : tactic
-macro_rules | `(tactic| is_empty) => `(tactic| apply Function.isEmpty (β := False))
-
 /--
 `Decidable'` is like `Decidable`, but allows arbitrary sorts.
 -/
@@ -26,9 +20,3 @@ instance [Repr α] : Repr (Decidable' α) where
   reprPrec da n := match da with
   | .inr a => ".inr " ++ reprPrec a n
   | .inl _ => ".inl _"
-
-theorem congr_arg₃
-(f : α → β → γ → δ) {x x' : α} {y y' : β} {z z' : γ}
-(hx : x = x') (hy : y = y') (hz : z = z')
-: f x y z = f x' y' z'
-:= by subst hx hy hz; rfl
diff --git a/Plfl/Init/Lemmas.lean b/Plfl/Init/Lemmas.lean
new file mode 100644
index 0000000..962c9e8
--- /dev/null
+++ b/Plfl/Init/Lemmas.lean
@@ -0,0 +1,9 @@
+module
+
+public section
+
+theorem congr_arg₃
+  (f : α → β → γ → δ) {x x' : α} {y y' : β} {z z' : γ}
+  (hx : x = x') (hy : y = y') (hz : z = z')
+  : f x y z = f x' y' z'
+  := by subst hx hy hz; rfl
diff --git a/Plfl/Init/Tactics.lean b/Plfl/Init/Tactics.lean
new file mode 100644
index 0000000..7ddfbd2
--- /dev/null
+++ b/Plfl/Init/Tactics.lean
@@ -0,0 +1,8 @@
+module
+public import Mathlib.Logic.IsEmpty.Defs
+
+/--
+`is_empty` converts `IsEmpty α` to `α → False`.
+-/
+syntax "is_empty" : tactic
+macro_rules | `(tactic| is_empty) => `(tactic| apply Function.isEmpty (β := False))
diff --git a/Plfl/Lambda.lean b/Plfl/Lambda.lean
index 628f79b..691074a 100644
--- a/Plfl/Lambda.lean
+++ b/Plfl/Lambda.lean
@@ -2,7 +2,6 @@ module
 
 -- https://plfa.github.io/Lambda/
 
-public import Plfl.Init
 import Mathlib.Data.Nat.Notation
 import Mathlib.Tactic.ApplyFun
 public import Mathlib.Logic.Embedding.Basic
@@ -214,7 +213,7 @@ namespace Term.Reduce
     apply_fun Clos'.toClos at h
     rwa [←toClos'_left_inv (x := a), ←toClos'_left_inv (x := b)]
 
-  instance Clos.embedsInClos' : (m —↠ n) ↪ (m —↠' n) where
+  def Clos.embedsInClos' : (m —↠ n) ↪ (m —↠' n) where
     toFun := toClos'
     inj' := toClos'_inj
 end Term.Reduce
diff --git a/Plfl/Lambda/Properties.lean b/Plfl/Lambda/Properties.lean
index 400a731..4de57f7 100644
--- a/Plfl/Lambda/Properties.lean
+++ b/Plfl/Lambda/Properties.lean
@@ -2,7 +2,7 @@ module
 
 -- https://plfa.github.io/Properties/
 
-public meta import Plfl.Init
+import Plfl.Init.Tactics
 public meta import Plfl.Lambda
 import Plfl.Lambda
 import Mathlib.Tactic.Basic
@@ -78,7 +78,7 @@ namespace Canonical
   /--
   The Canonical forms are exactly the well-typed values.
   -/
-  instance : Canonical v t ≃ (∅ ⊢ v ⦂ t) × Value v where
+  def equivWellTyped : Canonical v t ≃ (∅ ⊢ v ⦂ t) × Value v where
     toFun := wellTyped
     invFun := wellTypedInv
     left_inv := wellTyped_left_inv
@@ -162,7 +162,7 @@ namespace Progress
   @[simp] def toProgress' : Progress m → Progress' m | step r => inr ⟨_, r⟩ | done v => inl v
   @[simp] def fromProgress' : Progress' m → Progress m | inl v => done v | inr ⟨_, r⟩ => step r
 
-  instance : Progress m ≃ Progress' m where
+  def equivProgress' : Progress m ≃ Progress' m where
     toFun := toProgress'
     invFun := fromProgress'
     left_inv := by intro x; cases x <;> simp_all only [fromProgress', toProgress']
diff --git a/Plfl/More.lean b/Plfl/More.lean
index fce7bde..96ce053 100644
--- a/Plfl/More.lean
+++ b/Plfl/More.lean
@@ -2,7 +2,7 @@ module
 
 -- https://plfa.github.io/More/
 
-public import Plfl.Init
+import Plfl.Init.Tactics
 import Batteries.Tactic.Init
 public import Mathlib.Data.Matrix.Mul
 
diff --git a/Plfl/More/Bisimulation.lean b/Plfl/More/Bisimulation.lean
index 804ded3..b817c1b 100644
--- a/Plfl/More/Bisimulation.lean
+++ b/Plfl/More/Bisimulation.lean
@@ -2,7 +2,6 @@ module
 
 -- https://plfa.github.io/Bisimulation/
 
-public import Plfl.Init
 public import Plfl.More
 import Mathlib.Tactic.Basic
 
diff --git a/Plfl/More/DoubleSubst.lean b/Plfl/More/DoubleSubst.lean
index db6fcad..798d67b 100644
--- a/Plfl/More/DoubleSubst.lean
+++ b/Plfl/More/DoubleSubst.lean
@@ -4,7 +4,8 @@ module
 
 -- Adapted from <https://github.com/kaa1el/plfa_solution/blob/c5869a34bc4cac56cf970e0fe38874b62bd2dafc/src/plfa/demo/DoubleSubstitutionDeBruijn.agda>.
 
-public import Plfl.Init
+public import Plfl.Init.Tactics
+public import Plfl.Init.Lemmas
 public import Plfl.More
 
 @[expose] public section
diff --git a/Plfl/More/Inference.lean b/Plfl/More/Inference.lean
index 3ead3d4..3b73fdf 100644
--- a/Plfl/More/Inference.lean
+++ b/Plfl/More/Inference.lean
@@ -2,7 +2,9 @@ module
 
 -- https://plfa.github.io/Inference/
 
-public meta import Plfl.Init
+import Plfl.Init.Tactics
+meta import Plfl.Init.Decidable'
+public import Plfl.Init.Decidable'
 public import Plfl.More
 
 @[expose] public section
diff --git a/Plfl/Untyped.lean b/Plfl/Untyped.lean
index fe10bb0..1d2fd34 100644
--- a/Plfl/Untyped.lean
+++ b/Plfl/Untyped.lean
@@ -2,7 +2,6 @@ module
 
 -- https://plfa.github.io/Untyped/
 
-public import Plfl.Init
 import Mathlib.Data.Nat.Notation
 public import Mathlib.Logic.Equiv.Defs
 import Mathlib.Tactic.Basic
@@ -23,7 +22,7 @@ end Notation
 open Notation
 
 -- https://plfa.github.io/Untyped/#exercise-type-practice
-instance : Ty ≃ Unit where
+def equivTyUnit : Ty ≃ Unit where
   toFun _ := ()
   invFun _ := ✶
   left_inv _ := by simp only
@@ -50,7 +49,7 @@ namespace Notation
 end Notation
 
 -- https://plfa.github.io/Untyped/#exercise-context%E2%84%95-practice
-instance Context.equiv_nat : Context ≃ ℕ where
+def Context.equiv_nat : Context ≃ ℕ where
   toFun := List.length
   invFun := (List.replicate · (✶))
   left_inv := left_inv
diff --git a/Plfl/Untyped/BigStep.lean b/Plfl/Untyped/BigStep.lean
index bc84ad8..8110a4f 100644
--- a/Plfl/Untyped/BigStep.lean
+++ b/Plfl/Untyped/BigStep.lean
@@ -2,7 +2,6 @@ module
 
 -- https://plfa.github.io/BigStep/
 
-public import Plfl.Init
 public import Plfl.Untyped
 public import Plfl.Untyped.Substitution
 import Mathlib.Logic.Lemmas
diff --git a/Plfl/Untyped/Confluence.lean b/Plfl/Untyped/Confluence.lean
index d918805..257acba 100644
--- a/Plfl/Untyped/Confluence.lean
+++ b/Plfl/Untyped/Confluence.lean
@@ -2,7 +2,6 @@ module
 
 -- https://plfa.github.io/Confluence/
 
-public import Plfl.Init
 public import Plfl.Untyped
 public import Plfl.Untyped.Substitution
 
@@ -79,7 +78,7 @@ namespace PReduce
       _ —↠ l' □ m' := Untyped.Reduce.ap_congr₂ (toReduceClos rm)
 end PReduce
 
-instance instNonemptyPReduceReduceClos : (m ⇛* n) ≃ (m —↠ n) where
+def equivPReduceClosReduceClos : (m ⇛* n) ≃ (m —↠ n) where
   toFun := toFun
   invFun := invFun
   left_inv _ := by simp only
@@ -153,14 +152,14 @@ namespace Notation
 end Notation
 
 theorem par_triangle {m n : Γ ⊢ a} : (m ⇛ n) → (n ⇛ m⁺) := open PReduce in by
-intro
-| .var => exact .var
-| .lamβ pn pv => exact subst_par (par_subst₁σ (par_triangle pv)) (par_triangle pn)
-| .lamζ pn => exact lamζ (par_triangle pn)
-| .apξ pl pm => rename_i l l' m m'; match l with
-  | ‵ _ => exact apξ (par_triangle pl) (par_triangle pm)
-  | _ □ _ => exact apξ (par_triangle pl) (par_triangle pm)
-  | ƛ _  => have .lamζ pl := pl; exact lamβ (par_triangle pl) (par_triangle pm)
+  intro p; match p with
+  | .var => exact .var
+  | .lamβ pn pv => exact subst_par (par_subst₁σ (par_triangle pv)) (par_triangle pn)
+  | .lamζ pn => exact lamζ (par_triangle pn)
+  | .apξ pl pm => rename_i l l' m m'; match l with
+    | ‵ _ => exact apξ (par_triangle pl) (par_triangle pm)
+    | _ □ _ => exact apξ (par_triangle pl) (par_triangle pm)
+    | ƛ _ => match pl with | .lamζ pl => exact lamβ (par_triangle pl) (par_triangle pm)
 
 theorem par_diamond {m n n' : Γ ⊢ a} (p : m ⇛ n) (p' : m ⇛ n')
 : ∃ (l : Γ ⊢ a), (n ⇛ l) ∧ (n' ⇛ l)
@@ -189,6 +188,6 @@ theorem par_confluence {l m m' : Γ ⊢ a} (lm : l ⇛* m) (lm' : l ⇛* m')
 theorem confluence {l m m' : Γ ⊢ a} (lm : l —↠ m) (lm' : l —↠ m')
 : ∃ (n : Γ ⊢ a), (m —↠ n) ∧ (m' —↠ n)
 := by
-  let equiv := @instNonemptyPReduceReduceClos Γ a
+  let equiv := @equivPReduceClosReduceClos Γ a
   have ⟨n, mn, m'n⟩:= par_confluence (equiv.invFun lm) (equiv.invFun lm')
   exists n; exact ⟨equiv.toFun mn, equiv.toFun m'n⟩
diff --git a/Plfl/Untyped/Denotational.lean b/Plfl/Untyped/Denotational.lean
index c8f0896..71fb48c 100644
--- a/Plfl/Untyped/Denotational.lean
+++ b/Plfl/Untyped/Denotational.lean
@@ -2,7 +2,6 @@ module
 
 -- https://plfa.github.io/Denotational/
 
-public import Plfl.Init
 public import Plfl.Untyped
 public import Plfl.Untyped.Substitution
 import Mathlib.Data.Nat.Notation
diff --git a/Plfl/Untyped/Denotational/Adequacy.lean b/Plfl/Untyped/Denotational/Adequacy.lean
index f99b780..6ba298c 100644
--- a/Plfl/Untyped/Denotational/Adequacy.lean
+++ b/Plfl/Untyped/Denotational/Adequacy.lean
@@ -2,7 +2,6 @@ module
 
 -- https://plfa.github.io/Adequacy/
 
-public import Plfl.Init
 public import Plfl.Untyped.BigStep
 public import Plfl.Untyped.Denotational.Soundness
 public import Mathlib.Tactic
diff --git a/Plfl/Untyped/Denotational/Compositional.lean b/Plfl/Untyped/Denotational/Compositional.lean
index 66e18f0..0b483f6 100644
--- a/Plfl/Untyped/Denotational/Compositional.lean
+++ b/Plfl/Untyped/Denotational/Compositional.lean
@@ -2,7 +2,6 @@ module
 
 -- https://plfa.github.io/Compositional/
 
-public import Plfl.Init
 public import Plfl.Untyped.Denotational
 public import Mathlib.Order.BooleanAlgebra.Defs
 
diff --git a/Plfl/Untyped/Denotational/ContextualEquivalence.lean b/Plfl/Untyped/Denotational/ContextualEquivalence.lean
index 4f678a5..74186d7 100644
--- a/Plfl/Untyped/Denotational/ContextualEquivalence.lean
+++ b/Plfl/Untyped/Denotational/ContextualEquivalence.lean
@@ -2,7 +2,6 @@ module
 
 -- https://plfa.github.io/ContextualEquivalence/
 
-public import Plfl.Init
 public import Plfl.Untyped.Denotational.Adequacy
 
 @[expose] public section
diff --git a/Plfl/Untyped/Denotational/Soundness.lean b/Plfl/Untyped/Denotational/Soundness.lean
index cf60058..dc6b059 100644
--- a/Plfl/Untyped/Denotational/Soundness.lean
+++ b/Plfl/Untyped/Denotational/Soundness.lean
@@ -2,7 +2,6 @@ module
 
 -- https://plfa.github.io/Soundness/
 
-public import Plfl.Init
 public import Plfl.Untyped.Denotational.Compositional
 
 @[expose] public section
@@ -118,16 +117,16 @@ theorem subst_reflect {σ : Subst Γ Δ} (d : δ ⊢ l ￬ v) (h : ⟪σ⟫ m =
   induction d generalizing Γ with
   | bot => exists ⊥; exact ⟨subst_bot, .bot⟩
   | var => cases m with try contradiction
-    | var j => apply subst_reflect_var; convert Eval.var
+    | var j => apply subst_reflect_var; convert Eval.var using 1; exact h
   | ap d d' ih ih' => rename_i l' _ _ m'; cases m with try contradiction
-    | var => apply subst_reflect_var; convert d.ap d'
+    | var => apply subst_reflect_var; convert d.ap d' using 1; exact h
     | ap =>
       injection h; rename_i h h'
       let ⟨γ, dγ, dm⟩ := ih h; let ⟨γ', dγ', dm'⟩ := ih' h'; exists γ ⊔ γ'; constructor
       · exact subst_conj dγ dγ'
       · exact (sub_env dm <| Env.Sub.conjR₁ γ γ').ap (sub_env dm' <| Env.Sub.conjR₂ γ γ')
   | fn d ih => cases m with try contradiction
-    | var => apply subst_reflect_var; convert d.fn
+    | var => apply subst_reflect_var; convert d.fn using 1; exact h
     | lam =>
       injection h; rename_i h; let ⟨γ, dγ, dm⟩ := ih h; exists γ.init; constructor
       · intro i; exact rename_shift_reflect <| dγ i.s
diff --git a/Plfl/Untyped/Substitution.lean b/Plfl/Untyped/Substitution.lean
index 75b6c40..f4e6a82 100644
--- a/Plfl/Untyped/Substitution.lean
+++ b/Plfl/Untyped/Substitution.lean
@@ -2,7 +2,6 @@ module
 
 -- https://plfa.github.io/Substitution/#plfa_plfa-part2-Substitution-2341
 
-public import Plfl.Init
 public import Plfl.Untyped
 import Batteries.Tactic.Init
 import Batteries.Logic
@@ -179,7 +178,9 @@ section
     · rename_i x
       change ⟪fun {a} => subst₁σ m⟫ (exts (fun {a} => σ) (.s x)) = σ x
       simp only [exts, Subst.shift, rename_subst]
-      convert sub_ids (m := σ x) using 2
+      have : (fun {a} => subst₁σ m ∘ Lookup.s) = (fun {a} => @ids Δ a) := by
+        funext _ i; rfl
+      simp only [this, sub_ids]
 
   variable {n : Γ‚ ✶ ⊢ ✶} {m : Γ ⊢ ✶}
 
diff --git a/lake-manifest.json b/lake-manifest.json
index 4276e5e..81bcfa6 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -1,41 +1,21 @@
 {"version": "1.2.0",
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/leanprover-community/aesop",
+ [{"url": "https://github.com/leanprover-community/mathlib4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "558915ae105bfd8074e22d597613d1961822adc2",
-   "name": "aesop",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.30.0",
-   "inherited": false,
-   "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover-community/mathlib4",
-   "type": "git",
-   "subDir": null,
-   "scope": "leanprover-community",
-   "rev": "c5ea00351c28e24afc9f0f84379aa41082b1188f",
+   "rev": "fabf563a7c95a166b8d7b6efca11c8b4dc9d911f",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.30.0",
+   "inputRev": "v4.31.0",
    "inherited": false,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/batteries",
-   "type": "git",
-   "subDir": null,
-   "scope": "leanprover-community",
-   "rev": "32dc18cde3684679f3c003de608743b57498c56f",
-   "name": "batteries",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.30.0",
-   "inherited": true,
-   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a456461b368b71d2accd95234832cd9c174b5437",
+   "rev": "63045536fe95024e6c18fc7b48e03f506701c5bc",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "515cf9d0c00ece5e661f6de4326a53dedc1e8ea1",
+   "rev": "5c7542ed018c78194f1e2b903eaf6a792b74c03d",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,30 +45,50 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a84b3e2475d5c5ab979567b1ad8aea21b764bcf8",
+   "rev": "24b0d9dc081c5423f8eec7e866c441e5184f29d9",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.99",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/aesop",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "e3cb2f741431ce31bf73549fb52316a57368b06f",
+   "name": "aesop",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a6e6c34c4ef182f83b219a3a5a385f51f44bdc4c",
+   "rev": "f46324995fca5f0483b742e4eb4daec7f4ee50d2",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.30.0",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/batteries",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "fa08db58b30eb033edcdab331bba000827f9f785",
+   "name": "batteries",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "6b907cf12b2e445ccb7c24bc208ef04a1f39e84c",
+   "rev": "92564e5770e4d09f2d86dfbf8ada1e9c715b384c",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.30.0",
+   "inputRev": "v4.31.0",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "plfl",
diff --git a/lakefile.toml b/lakefile.toml
index c542f7f..a846618 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -15,13 +15,13 @@ maxSynthPendingDepth = 3    # same as mathlib, changes behaviour of typeclass in
 [[require]]
 name = "mathlib"
 scope = "leanprover-community"
-rev = "v4.30.0"
+rev = "v4.31.0"
 # git = "https://github.com/leanprover-community/mathlib4.git"
 
-[[require]]
-name = "aesop"
-scope = "leanprover-community"
-rev = "v4.30.0"
+# [[require]]
+# name = "aesop"
+# scope = "leanprover-community"
+# rev = "v4.31.0"
 # git = "https://github.com/JLimperg/aesop"
 
 [[lean_lib]]
diff --git a/lean-toolchain b/lean-toolchain
index af9e5d3..18640c8 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.30.0
+leanprover/lean4:v4.31.0