diff --git a/Pdl.lean b/Pdl.lean
index f181795..734efe2 100644
--- a/Pdl.lean
+++ b/Pdl.lean
@@ -1,6 +1,7 @@
 -- This module serves as the root of the `Pdl` library.
 -- Import modules here that should be built as part of the library.
 import «Pdl».Syntax
+import «Pdl».Vocab
 import «Pdl».Semantics
 import «Pdl».Star
 import «Pdl».Discon
diff --git a/Pdl/Interpolation.lean b/Pdl/Interpolation.lean
index 4d3ad71..363c1d3 100644
--- a/Pdl/Interpolation.lean
+++ b/Pdl/Interpolation.lean
@@ -1,4 +1,7 @@
+import Mathlib.Data.Finset.Basic
+
 import Pdl.Syntax
+import Pdl.Vocab
 import Pdl.Semantics
 
 open HasVocabulary vDash
diff --git a/Pdl/Semantics.lean b/Pdl/Semantics.lean
index 0ac901a..96f75e7 100644
--- a/Pdl/Semantics.lean
+++ b/Pdl/Semantics.lean
@@ -1,7 +1,8 @@
-import Mathlib.Order.CompleteLattice
-import Mathlib.Order.FixedPoints
+import Mathlib.Data.Finset.Basic
 import Mathlib.Data.Set.Lattice
 import Mathlib.Logic.Relation
+import Mathlib.Order.CompleteLattice
+import Mathlib.Order.FixedPoints
 
 import Pdl.Syntax
 
diff --git a/Pdl/Syntax.lean b/Pdl/Syntax.lean
index 25ddf1b..0f2dbdb 100644
--- a/Pdl/Syntax.lean
+++ b/Pdl/Syntax.lean
@@ -1,7 +1,4 @@
-import Std.Classes.SetNotation -- provides Union
-
-import Mathlib.Data.Finset.Basic -- this import affects unrelated stuff below O.o
--- see https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/induction.20for.20mutually.20inductive.20types/near/395082787
+import Mathlib.Order.BoundedOrder
 
 mutual
   inductive Formula : Type
@@ -10,23 +7,16 @@ mutual
     | neg : Formula → Formula
     | and : Formula → Formula → Formula
     | box : Program → Formula → Formula
-    deriving Repr -- DecidableEq is not derivable here?
+    deriving Repr, DecidableEq
   inductive Program : Type
     | atom_prog : Char → Program
     | sequence : Program → Program → Program
     | union : Program → Program → Program
     | star : Program → Program
     | test : Formula → Program
-    deriving Repr -- DecidableEq is not derivable here?
+    deriving Repr, DecidableEq -- is not derivable here?
 end
 
--- TODO: update the above once we have a newer Lean version
--- including https://github.com/leanprover/lean4/pull/2591
-
--- needed for unions etc
-instance decEqFormula : DecidableEq Formula := sorry
-instance decEqProgram : DecidableEq Program := sorry
-
 -- Notation and abbreviations
 
 @[simp]
@@ -47,9 +37,11 @@ notation "·" c => Formula.atom_prop c
 notation "·" c => Program.atom_prog c
 prefix:11 "~" => Formula.neg
 
--- TODO: use class instances to avoid overwriting ⊥ and ⊤
-notation "⊥" => Formula.bottom
-notation "⊤" => Formula.neg Formula.bottom
+@[simp]
+instance Formula.instBot : Bot Formula := ⟨Formula.bottom⟩
+@[simp]
+instance Formula.insTop : Top Formula := ⟨Formula.neg Formula.bottom⟩
+
 infixr:66 "⋀" => Formula.and
 infixr:60 "⋁" => Formula.or
 notation:55 φ:56 " ↣ " ψ:55 => ~φ ⋀ (~ψ)
@@ -114,45 +106,14 @@ termination_by -- silly but needed?!
   mOfProgram p => sizeOf p
   mOfFormula f => sizeOf f
 
-
--- VOCAB
-
-mutual
-  def vocabOfProgram : Program → Finset Char
-    | ·c => {c}
-    | α;β => vocabOfProgram α ∪ vocabOfProgram β
-    | Program.union α β => vocabOfProgram α ∪ vocabOfProgram β
-    | ∗α => vocabOfProgram α
-    | ✓ φ => vocabOfFormula φ
-  def vocabOfFormula : Formula → Finset Char
-    | ⊥ => ∅
-    | ·c => {c}
-    | ~φ => vocabOfFormula φ
-    | φ⋀ψ => vocabOfFormula φ ∪ vocabOfFormula ψ
-    | ⌈α⌉ φ => vocabOfProgram α ∪ vocabOfFormula φ
-end
-termination_by -- silly but needed?!
-  vocabOfProgram p => sizeOf p
-  vocabOfFormula f => sizeOf f
-
-def vocabOfSetFormula : Finset Formula → Finset Char
-  | X => X.biUnion vocabOfFormula
-
-class HasVocabulary (α : Type) where
-  voc : α → Finset Char
-
-instance formulaHasVocabulary : HasVocabulary Formula := ⟨vocabOfFormula⟩
-instance programHasVocabulary : HasVocabulary Program := ⟨vocabOfProgram⟩
-instance finsetFormulaHasVocabulary : HasVocabulary (Finset Formula) := ⟨vocabOfSetFormula⟩
-
-lemma boxes_last : (~⌈a⌉Formula.boxes (as ++ [c]) P) = (~⌈a⌉Formula.boxes as (⌈c⌉P)) :=
+theorem boxes_last : (~⌈a⌉Formula.boxes (as ++ [c]) P) = (~⌈a⌉Formula.boxes as (⌈c⌉P)) :=
   by
   induction as
   · simp
   · simp at *
     assumption
 
-lemma boxes_append : Formula.boxes (as ++ bs) P = Formula.boxes as (Formula.boxes bs P) :=
+theorem boxes_append : Formula.boxes (as ++ bs) P = Formula.boxes as (Formula.boxes bs P) :=
   by
   induction as
   · simp
diff --git a/Pdl/Vocab.lean b/Pdl/Vocab.lean
new file mode 100644
index 0000000..a651bc0
--- /dev/null
+++ b/Pdl/Vocab.lean
@@ -0,0 +1,32 @@
+import Pdl.Syntax
+
+import Mathlib.Data.Finset.Basic
+
+-- VOCAB
+mutual
+  def vocabOfProgram : Program → Finset Char
+    | ·c => {c}
+    | α;β => vocabOfProgram α ∪ vocabOfProgram β
+    | Program.union α β => vocabOfProgram α ∪ vocabOfProgram β
+    | ∗α => vocabOfProgram α
+    | ✓ φ => vocabOfFormula φ
+  def vocabOfFormula : Formula → Finset Char
+    | ⊥ => ∅
+    | ·c => {c}
+    | ~φ => vocabOfFormula φ
+    | φ⋀ψ => vocabOfFormula φ ∪ vocabOfFormula ψ
+    | ⌈α⌉ φ => vocabOfProgram α ∪ vocabOfFormula φ
+end
+termination_by -- silly but needed?!
+  vocabOfProgram p => sizeOf p
+  vocabOfFormula f => sizeOf f
+
+def vocabOfSetFormula : Finset Formula → Finset Char
+  | X => X.biUnion vocabOfFormula
+
+class HasVocabulary (α : Type) where
+  voc : α → Finset Char
+
+instance formulaHasVocabulary : HasVocabulary Formula := ⟨vocabOfFormula⟩
+instance programHasVocabulary : HasVocabulary Program := ⟨vocabOfProgram⟩
+instance finsetFormulaHasVocabulary : HasVocabulary (Finset Formula) := ⟨vocabOfSetFormula⟩
diff --git a/lake-manifest.json b/lake-manifest.json
index f6a917c..c6f1bb8 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -4,13 +4,21 @@
  [{"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "be0d066cb7381532d79a03e56bfd664ecd6e69ba",
+    "rev": "9eb5aaff128911772f3564ce032b44a94d5f8ba7",
     "opts": {},
     "name": "mathlib",
     "inputRev?": null,
     "inherited": false}},
   {"git":
-   {"url": "https://github.com/gebner/quote4",
+   {"url": "https://github.com/leanprover/std4",
+    "subDir?": null,
+    "rev": "fb56324020c8e4f3d451e8901b290dea82c072ae",
+    "opts": {},
+    "name": "std",
+    "inputRev?": "main",
+    "inherited": true}},
+  {"git":
+   {"url": "https://github.com/leanprover-community/quote4",
     "subDir?": null,
     "rev": "a387c0eb611857e2460cf97a8e861c944286e6b2",
     "opts": {},
@@ -18,15 +26,15 @@
     "inputRev?": "master",
     "inherited": true}},
   {"git":
-   {"url": "https://github.com/JLimperg/aesop",
+   {"url": "https://github.com/leanprover-community/aesop",
     "subDir?": null,
-    "rev": "4f8b397237411249930791f1cba0a9d2880a02dd",
+    "rev": "9dc4a1097a690216eaa7cf2d2290efd447e60d7a",
     "opts": {},
     "name": "aesop",
     "inputRev?": "master",
     "inherited": true}},
   {"git":
-   {"url": "https://github.com/mhuisi/lean4-cli.git",
+   {"url": "https://github.com/leanprover/lean4-cli",
     "subDir?": null,
     "rev": "39229f3630d734af7d9cfb5937ddc6b41d3aa6aa",
     "opts": {},
@@ -34,19 +42,11 @@
     "inputRev?": "nightly",
     "inherited": true}},
   {"git":
-   {"url": "https://github.com/leanprover/std4",
-    "subDir?": null,
-    "rev": "f2df4ab8c0726fce3bafb73a5727336b0c3120ea",
-    "opts": {},
-    "name": "std",
-    "inputRev?": "main",
-    "inherited": true}},
-  {"git":
-   {"url": "https://github.com/EdAyers/ProofWidgets4",
+   {"url": "https://github.com/leanprover-community/ProofWidgets4",
     "subDir?": null,
-    "rev": "9f68f14df384f43b74aeb2908b97ae54a0ad9d95",
+    "rev": "5382e38eca1e2537d75d4c4705a9e744424b0037",
     "opts": {},
     "name": "proofwidgets",
-    "inputRev?": "v0.0.17",
+    "inputRev?": "v0.0.19",
     "inherited": true}}],
  "name": "pdl"}
diff --git a/lean-toolchain b/lean-toolchain
index 400394a..183a307 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.2.0-rc1
+leanprover/lean4:v4.2.0-rc4