diff --git a/Pdl/Discon.lean b/Pdl/Discon.lean
index b8a4f20..dc87c3d 100644
--- a/Pdl/Discon.lean
+++ b/Pdl/Discon.lean
@@ -223,26 +223,24 @@ theorem mapCon_mapForall (M : KripkeModel W) w φ
     · use a, b
     · rw [conEval]; intro f; tauto
 
-open HasVocabulary
-
 theorem in_voc_dis n (L : List Formula) :
-    n ∈ voc (dis L) ↔ ∃ φ ∈ L, n ∈ voc φ := by
+    n ∈ (dis L).voc ↔ ∃ φ ∈ L, n ∈ φ.voc := by
   induction L
-  · simp [voc, dis, vocabOfFormula]
+  · simp [dis, Formula.voc]
   case cons h t IH =>
     induction t -- needed to select case in `dis`
-    · simp [voc, dis, vocabOfFormula]
+    · simp [dis, Formula.voc]
     case cons h t IH =>
-      simp [voc, dis, vocabOfFormula] at *
+      simp [dis, Formula.voc] at *
       rw [← IH]
 
 theorem in_voc_con n (L : List Formula) :
-    n ∈ voc (Con L) ↔ ∃ φ ∈ L, n ∈ voc φ := by
+    n ∈ (Con L).voc ↔ ∃ φ ∈ L, n ∈ φ.voc := by
   induction L
-  · simp [voc, Con, vocabOfFormula]
+  · simp [Con, Formula.voc]
   case cons h t IH =>
     induction t -- needed to select case in `Con`
-    · simp [voc, Con, vocabOfFormula]
+    · simp [Con, Formula.voc]
     case cons h t IH =>
-      simp [voc, Con, vocabOfFormula] at *
+      simp [Con, Formula.voc] at *
       rw [← IH]
diff --git a/Pdl/Fresh.lean b/Pdl/Fresh.lean
index 120e9ab..39b83a8 100644
--- a/Pdl/Fresh.lean
+++ b/Pdl/Fresh.lean
@@ -18,12 +18,10 @@ mutual
     | ?'φ  => freshVarForm φ
 end
 
-open HasVocabulary
-
 mutual
-theorem freshVarForm_is_larger (φ) : ∀ n ∈ (vocabOfFormula φ).atomProps, n < freshVarForm φ := by
+theorem freshVarForm_is_larger (φ) : ∀ n ∈ φ.voc.atomProps, n < freshVarForm φ := by
   cases φ
-  all_goals simp [freshVarForm, voc, vocabOfFormula, not_or, Vocab.atomProps]
+  all_goals simp [freshVarForm, Formula.voc, not_or, Vocab.atomProps]
   case neg φ =>
     have IH := freshVarForm_is_larger φ
     simp [Vocab.atomProps] at *
@@ -39,9 +37,9 @@ theorem freshVarForm_is_larger (φ) : ∀ n ∈ (vocabOfFormula φ).atomProps, n
     simp [Vocab.atomProps] at *
     aesop
 
-theorem freshVarProg_is_larger (α) : ∀ n ∈ (vocabOfProgram α).atomProps, n < freshVarProg α := by
+theorem freshVarProg_is_larger (α) : ∀ n ∈ α.voc.atomProps, n < freshVarProg α := by
   cases α
-  all_goals simp [freshVarProg, voc, vocabOfProgram, Vocab.atomProps]
+  all_goals simp [freshVarProg, Program.voc, Vocab.atomProps]
   case union α β =>
     have IHα := freshVarProg_is_larger α
     have IHβ := freshVarProg_is_larger β
@@ -62,17 +60,17 @@ theorem freshVarProg_is_larger (α) : ∀ n ∈ (vocabOfProgram α).atomProps, n
     aesop
 end
 
-theorem freshVarForm_is_fresh (φ) : Sum.inl (freshVarForm φ) ∉ voc φ := by
+theorem freshVarForm_is_fresh (φ) : Sum.inl (freshVarForm φ) ∉ φ.voc := by
   have := freshVarForm_is_larger φ
-  simp [freshVarForm, voc, vocabOfFormula, Vocab.atomProps] at *
+  simp [freshVarForm, Formula.voc, Vocab.atomProps] at *
   by_contra hyp
   specialize this (freshVarForm φ)
   have := Nat.lt_irrefl (freshVarForm φ)
   tauto
 
-theorem freshVarProg_is_fresh (α) : Sum.inl (freshVarProg α) ∉ vocabOfProgram α := by
+theorem freshVarProg_is_fresh (α) : Sum.inl (freshVarProg α) ∉ α.voc := by
   have := freshVarProg_is_larger α
-  simp [freshVarProg, voc, vocabOfFormula, Vocab.atomProps] at *
+  simp [freshVarProg, Formula.voc, Vocab.atomProps] at *
   by_contra hyp
   specialize this (freshVarProg α)
   have := Nat.lt_irrefl (freshVarProg α)
diff --git a/Pdl/Interpolation.lean b/Pdl/Interpolation.lean
index a421482..b333193 100644
--- a/Pdl/Interpolation.lean
+++ b/Pdl/Interpolation.lean
@@ -2,10 +2,10 @@ import Mathlib.Data.Finset.Basic
 
 import Pdl.PartInterpolation
 
-open HasVocabulary vDash HasSat
+open vDash HasSat
 
 def Interpolant (φ : Formula) (ψ : Formula) (θ : Formula) :=
-  voc θ ⊆ voc φ ∩ voc ψ  ∧  φ ⊨ θ  ∧  θ ⊨ ψ
+  θ.voc ⊆ φ.voc ∩ ψ.voc  ∧  φ ⊨ θ  ∧  θ ⊨ ψ
 
 theorem interpolation : ∀ (φ ψ : Formula), φ⊨ψ → ∃ θ : Formula, Interpolant φ ψ θ :=
   by
@@ -23,8 +23,8 @@ theorem interpolation : ∀ (φ ψ : Formula), φ⊨ψ → ∃ θ : Formula, Int
   use θ
   constructor
   · intro f f_in
-    simp [voc, jvoc, vocabOfFormula, Vocab.fromList] at pI_prop f_in
-    simp only [voc, Finset.mem_inter]
+    simp [jvoc, Formula.voc, Vocab.fromList] at pI_prop f_in
+    simp only [Finset.mem_inter]
     have := pI_prop.1 f_in
     aesop
   constructor
diff --git a/Pdl/LocalTableau.lean b/Pdl/LocalTableau.lean
index e87b1ba..31d88cf 100644
--- a/Pdl/LocalTableau.lean
+++ b/Pdl/LocalTableau.lean
@@ -13,16 +13,11 @@ open HasLength
 /-- In nodes we optionally have a negated loaded formula on the left or right. -/
 abbrev Olf := Option (NegLoadFormula ⊕ NegLoadFormula)
 
-open HasVocabulary
-
 @[simp]
-def vocabOfOlf : Olf → Vocab
+def Olf.voc : Olf → Vocab
 | none => {}
-| some (Sum.inl nlf) => voc nlf
-| some (Sum.inr nlf) => voc nlf
-
-@[simp]
-instance : HasVocabulary Olf := ⟨ vocabOfOlf ⟩
+| some (Sum.inl nlf) => nlf.voc
+| some (Sum.inr nlf) => nlf.voc
 
 /-- A tableau node has two lists of formulas and an `Olf`. -/
 -- TODO: rename `TNode` to `Sequent`
@@ -788,7 +783,7 @@ theorem unfoldBox.decreases_lmOf_nonAtomic {α : Program} {φ : Formula} {X : Li
   have ubc := unfoldBoxContent (α) φ X X_in ψ ψ_in_X
   cases α <;> simp [Program.isAtomic] at *
   case sequence α β =>
-    rcases ubc with one | ⟨τ, τ_in, def_ψ⟩ | ⟨a, δ, def_ψ⟩
+    rcases ubc with one | ⟨τ, τ_in, def_ψ⟩ | ⟨a, δ, def_ψ, _⟩
     · subst_eqs; linarith
     · subst def_ψ
       suffices lmOfFormula (~τ) < (List.map (fun x => lmOfFormula (~ (x.1))) (testsOfProgram (α;'β)).attach).sum.succ by
@@ -803,7 +798,7 @@ theorem unfoldBox.decreases_lmOf_nonAtomic {α : Program} {φ : Formula} {X : Li
     · subst def_ψ
       simp [lmOfFormula]
   case union α β => -- based on sequence case
-    rcases ubc with one | ⟨τ, τ_in, def_ψ⟩ | ⟨a, δ, def_ψ⟩
+    rcases ubc with one | ⟨τ, τ_in, def_ψ⟩ | ⟨a, δ, def_ψ, _⟩
     · subst_eqs; linarith
     · subst def_ψ
       suffices lmOfFormula (~τ) < (List.map (fun x => lmOfFormula (~ (x.1))) (testsOfProgram (α⋓β)).attach).sum.succ by
@@ -817,7 +812,7 @@ theorem unfoldBox.decreases_lmOf_nonAtomic {α : Program} {φ : Formula} {X : Li
     · subst def_ψ
       simp [lmOfFormula]
   case star β => -- based on sequence case
-    rcases ubc with one | ⟨τ, τ_in, def_ψ⟩ | ⟨a, δ, def_ψ⟩
+    rcases ubc with one | ⟨τ, τ_in, def_ψ⟩ | ⟨a, δ, def_ψ, _⟩
     · subst_eqs; linarith
     · subst def_ψ
       suffices lmOfFormula (~τ) < (List.map (fun x => lmOfFormula (~ (x.1))) (testsOfProgram (∗β)).attach).sum.succ by
@@ -831,7 +826,7 @@ theorem unfoldBox.decreases_lmOf_nonAtomic {α : Program} {φ : Formula} {X : Li
     · subst def_ψ
       simp [lmOfFormula]
   case test τ0 => -- based on sequence case
-    rcases ubc with one | ⟨τ, τ_in, def_ψ⟩ | ⟨a, δ, def_ψ⟩
+    rcases ubc with one | ⟨τ, τ_in, def_ψ⟩ | ⟨a, δ, def_ψ, _⟩
     · subst_eqs; linarith
     · subst def_ψ
       suffices lmOfFormula (~τ) < (List.map (fun x => lmOfFormula (~ (x.1))) (testsOfProgram (?'τ0)).attach).sum.succ by
diff --git a/Pdl/PartInterpolation.lean b/Pdl/PartInterpolation.lean
index e2b8a82..2fe432b 100644
--- a/Pdl/PartInterpolation.lean
+++ b/Pdl/PartInterpolation.lean
@@ -3,7 +3,7 @@ import Mathlib.Data.Finset.Basic
 import Pdl.Completeness
 import Pdl.Distance
 
-open HasVocabulary HasSat
+open HasSat
 
 def Olf.toForms : Olf → List Formula
 | none => []
@@ -17,24 +17,24 @@ def TNode.right (X : TNode) : List Formula := X.R ++ X.O.toForms
 
 /-- Joint vocabulary of all parts of a TNode. -/
 @[simp]
-def jvoc (X : TNode) : Vocab := voc (X.left) ∩ voc (X.right)
+def jvoc (X : TNode) : Vocab := (X.left).fvoc ∩ (X.right).fvoc
 
 def isPartInterpolant (X : TNode) (θ : Formula) :=
-  voc θ ⊆ jvoc X ∧ (¬ satisfiable ((~θ) :: X.left) ∧ ¬ satisfiable (θ :: X.right))
+  θ.voc ⊆ jvoc X ∧ (¬ satisfiable ((~θ) :: X.left) ∧ ¬ satisfiable (θ :: X.right))
 
 def PartInterpolant (N : TNode) := Subtype <| isPartInterpolant N
 
 -- TODO move elsewhere
-theorem Formula.voc_boxes : vocabOfFormula (⌈⌈δ⌉⌉φ) =
-    Vocab.fromList (δ.map vocabOfProgram) ∪ vocabOfFormula φ := by sorry
+theorem Formula.voc_boxes : (⌈⌈δ⌉⌉φ).voc = δ.pvoc ∪ φ.voc := by
+  sorry
 
 -- move to UnfoldBox.lean ?
 theorem unfoldBox_voc {x α φ} {L} (L_in : L ∈ unfoldBox α φ) {ψ} (ψ_in : ψ ∈ L)
-    (x_in_voc_ψ : x ∈ vocabOfFormula ψ) : x ∈ vocabOfProgram α ∨ x ∈ vocabOfFormula φ := by
-  rcases unfoldBoxContent _ _ _ L_in _ ψ_in with ψ_def | ⟨τ, τ_in, ψ_def⟩ | ⟨a, δ, ψ_def⟩
+    (x_in_voc_ψ : x ∈ ψ.voc) : x ∈ α.voc ∨ x ∈ φ.voc := by
+  rcases unfoldBoxContent _ _ _ L_in _ ψ_in with ψ_def | ⟨τ, τ_in, ψ_def⟩ | ⟨a, δ, ψ_def, _⟩
   all_goals subst ψ_def
   · right; exact x_in_voc_ψ
-  · simp only [vocabOfFormula] at x_in_voc_ψ
+  · simp only [Formula.voc] at x_in_voc_ψ
     left
     -- PROBLEM: here and in next case we need the stronger version of `unfoldBoxContent`.
     sorry
@@ -44,7 +44,7 @@ theorem unfoldBox_voc {x α φ} {L} (L_in : L ∈ unfoldBox α φ) {ψ} (ψ_in :
 
 -- move to UnfoldDia.lean ?
 theorem unfoldDiamond_voc {x α φ} {L} (L_in : L ∈ unfoldDiamond α φ) {ψ} (ψ_in : ψ ∈ L)
-    (x_in_voc_ψ : x ∈ vocabOfFormula ψ) : x ∈ vocabOfProgram α ∨ x ∈ vocabOfFormula φ := by
+    (x_in_voc_ψ : x ∈ ψ.voc) : x ∈ α.voc ∨ x ∈ φ.voc := by
   simp [unfoldDiamond, Yset] at L_in
   -- TODO use unfoldDiamondContent here instead?
   rcases L_in with ⟨Fs, δ, in_H, def_L⟩
@@ -56,12 +56,11 @@ theorem unfoldDiamond_voc {x α φ} {L} (L_in : L ∈ unfoldDiamond α φ) {ψ}
     have := H_mem_test α ψ in_H hyp
     rcases this with ⟨τ, τ_in, ψ_def⟩
     subst ψ_def
-    -- need lemma that voc-of-testsOfProgram is subset of voc
-    sorry
+    exact testsOfProgram.voc α τ_in x_in_voc_ψ
   case inr ψ_def =>
     have := H_mem_sequence
     subst ψ_def
-    simp only [vocabOfFormula, Formula.voc_boxes, Finset.mem_union] at x_in_voc_ψ
+    simp only [Formula.voc, Formula.voc_boxes, Finset.mem_union] at x_in_voc_ψ
     cases x_in_voc_ψ
     case inl hyp =>
       left
@@ -73,7 +72,7 @@ theorem unfoldDiamond_voc {x α φ} {L} (L_in : L ∈ unfoldDiamond α φ) {ψ}
       assumption
 
 theorem localRule_does_not_increase_vocab_L (rule : LocalRule (Lcond, Rcond, Ocond) ress) :
-    ∀ res ∈ ress, voc res.1 ⊆ voc Lcond := by
+    ∀ res ∈ ress, res.1.fvoc ⊆ Lcond.fvoc := by
   intro res ress_in_ress x x_in_res
   cases rule
   case oneSidedL ress orule =>
@@ -110,12 +109,12 @@ theorem localRule_does_not_increase_vocab_L (rule : LocalRule (Lcond, Rcond, Oco
   · aesop
 
 theorem localRule_does_not_increase_vocab_R (rule : LocalRule (Lcond, Rcond, Ocond) ress) :
-    ∀ res ∈ ress, voc res.2.1 ⊆ voc Rcond := by
+    ∀ res ∈ ress, res.2.1.fvoc ⊆ Rcond.fvoc := by
   -- should be dual to _L version
   sorry
 
 theorem localRule_does_not_increase_vocab_O (rule : LocalRule (Lcond, Rcond, Ocond) ress) :
-    ∀ res ∈ ress, voc res.2.2 ⊆ voc Ocond := by
+    ∀ res ∈ ress, res.2.2.voc ⊆ Ocond.voc := by
   sorry
 
 theorem localRuleApp_does_not_increase_jvoc (ruleA : LocalRuleApp X C) :
diff --git a/Pdl/Substitution.lean b/Pdl/Substitution.lean
index d6b7113..6dc4acf 100644
--- a/Pdl/Substitution.lean
+++ b/Pdl/Substitution.lean
@@ -48,33 +48,32 @@ theorem repl_in_dis : repl_in_F x ψ (dis l) = dis (l.map (repl_in_F x ψ)) := b
       simp [dis]
       apply repl_in_dis
 
-open HasVocabulary
-
 mutual
 theorem repl_in_F_non_occ_eq {x φ ρ} :
-    (Sum.inl x) ∉ voc φ → repl_in_F x ρ φ = φ := by
+    (Sum.inl x) ∉ φ.voc → repl_in_F x ρ φ = φ := by
   intro x_notin_phi
   cases φ
   case bottom => simp
   case atom_prop c =>
     simp only [repl_in_F, beq_iff_eq, ite_eq_right_iff]
-    intro c_is_x; simp [voc,vocabOfFormula] at *; subst_eqs; tauto
+    intro c_is_x; simp [Formula.voc] at *; subst_eqs; tauto
   case neg φ0 =>
-    simp [voc,vocabOfFormula] at *
+    simp [Formula.voc] at *
     apply repl_in_F_non_occ_eq; tauto
   case and φ1 φ2 =>
-    simp [voc,vocabOfFormula] at *
+    simp [Formula.voc] at *
     constructor <;> (apply repl_in_F_non_occ_eq ; tauto)
   case box α φ0 =>
-    simp [voc,vocabOfFormula] at *
+    simp [Formula.voc] at *
     constructor
     · apply repl_in_P_non_occ_eq; tauto
     · apply repl_in_F_non_occ_eq; tauto
+
 theorem repl_in_P_non_occ_eq {x α ρ} :
-    (Sum.inl x) ∉ voc α → repl_in_P x ρ α = α := by
+    (Sum.inl x) ∉ α.voc → repl_in_P x ρ α = α := by
   intro x_notin_alpha
   cases α
-  all_goals simp [voc,vocabOfProgram] at *
+  all_goals simp [Program.voc] at *
   case sequence β γ =>
     constructor <;> (apply repl_in_P_non_occ_eq; tauto)
   case union β γ =>
@@ -86,7 +85,7 @@ theorem repl_in_P_non_occ_eq {x α ρ} :
 end
 
 theorem repl_in_boxes_non_occ_eq_neg (δ : List Program) :
-    (Sum.inl x) ∉ voc δ → repl_in_F x ψ (⌈⌈δ⌉⌉~·x) = ⌈⌈δ⌉⌉~ψ := by
+    (Sum.inl x) ∉ Vocab.fromList (δ.map Program.voc) → repl_in_F x ψ (⌈⌈δ⌉⌉~·x) = ⌈⌈δ⌉⌉~ψ := by
   intro nonOcc
   induction δ
   · simp
@@ -94,13 +93,13 @@ theorem repl_in_boxes_non_occ_eq_neg (δ : List Program) :
     simp only [Formula.boxes, List.foldr_cons, repl_in_F, Formula.box.injEq]
     constructor
     · apply repl_in_P_non_occ_eq
-      simp_all [voc, vocabOfProgram, Vocab.fromList]
+      simp_all [Program.voc, Vocab.fromList]
     · apply IH
       clear IH
-      simp_all [voc, vocabOfProgram, Vocab.fromList]
+      simp_all [Program.voc, Vocab.fromList]
 
 theorem repl_in_boxes_non_occ_eq_pos (δ : List Program) :
-    (Sum.inl x) ∉ voc δ → repl_in_F x ψ (⌈⌈δ⌉⌉·x) = ⌈⌈δ⌉⌉ψ := by
+    (Sum.inl x) ∉ Vocab.fromList (δ.map Program.voc) → repl_in_F x ψ (⌈⌈δ⌉⌉·x) = ⌈⌈δ⌉⌉ψ := by
   intro nonOcc
   induction δ
   · simp
@@ -108,13 +107,13 @@ theorem repl_in_boxes_non_occ_eq_pos (δ : List Program) :
     simp only [Formula.boxes, List.foldr_cons, repl_in_F, Formula.box.injEq]
     constructor
     · apply repl_in_P_non_occ_eq
-      simp_all [voc, vocabOfProgram, Vocab.fromList]
+      simp_all [Program.voc, Vocab.fromList]
     · apply IH
       clear IH
-      simp_all [voc, vocabOfProgram, Vocab.fromList]
+      simp_all [Program.voc, Vocab.fromList]
 
 theorem repl_in_list_non_occ_eq (F : List Formula) :
-     (Sum.inl x) ∉ voc F → F.map (repl_in_F x ρ) = F := by
+     (Sum.inl x) ∉ Vocab.fromList (F.map Formula.voc) → F.map (repl_in_F x ρ) = F := by
   intro nonOcc
   induction F
   · simp
@@ -122,11 +121,11 @@ theorem repl_in_list_non_occ_eq (F : List Formula) :
     simp only [List.map_cons, List.cons.injEq]
     constructor
     · apply repl_in_F_non_occ_eq
-      simp [voc, vocabOfProgram, Vocab.fromList] at *
+      simp [Program.voc, Vocab.fromList] at *
       exact nonOcc.left
     · apply IH
       clear IH
-      simp_all [voc, vocabOfProgram, Vocab.fromList]
+      simp_all [Program.voc, Vocab.fromList]
 
 /-- Overwrite the valuation of `x` with the current value of `ψ` in a model. -/
 def repl_in_model (x : Nat) (ψ : Formula) : KripkeModel W → KripkeModel W
diff --git a/Pdl/UnfoldBox.lean b/Pdl/UnfoldBox.lean
index 8e88660..a299dfc 100644
--- a/Pdl/UnfoldBox.lean
+++ b/Pdl/UnfoldBox.lean
@@ -8,8 +8,6 @@ import Pdl.Fresh
 import Pdl.Star
 -- import Pdl.FischerLadner
 
-open HasVocabulary
-
 -- ### Preparation for Boxes: Test Profiles
 
 -- def TestProfile (α : Program) : Type := {L // L ∈ (testsOfProgram α).sublists}
@@ -318,13 +316,13 @@ theorem F_goes_down : φ ∈ F α ℓ → lengthOfFormula φ < lengthOfProgram 
     · simp_all
     · simp_all
 
-theorem keepFreshF α ℓ (x_notin : x ∉ voc α) : ∀ φ ∈ F α ℓ, x ∉ voc φ := by
+theorem keepFreshF α ℓ (x_notin : x ∉ α.voc) : ∀ φ ∈ F α ℓ, x ∉ φ.voc := by
   intro φ φ_in
   cases α
   all_goals
-    simp [F, voc, vocabOfFormula, vocabOfProgram, Vocab.fromList] at *
+    simp [F, Formula.voc, Program.voc, Vocab.fromList] at *
   case test τ =>
-    cases em (ℓ ⟨τ, by simp [testsOfProgram]⟩) <;> simp_all [vocabOfFormula]
+    cases em (ℓ ⟨τ, by simp [testsOfProgram]⟩) <;> simp_all [Formula.voc]
   case sequence α β =>
     have := keepFreshF α ℓ x_notin.1
     have := keepFreshF β ℓ x_notin.2
@@ -337,17 +335,17 @@ theorem keepFreshF α ℓ (x_notin : x ∉ voc α) : ∀ φ ∈ F α ℓ, x ∉
     have := keepFreshF α ℓ x_notin
     aesop
 
-theorem keepFreshP α ℓ (x_notin : x ∉ voc α) : ∀ δ ∈ P α ℓ, x ∉ voc δ := by
+theorem keepFreshP α ℓ (x_notin : x ∉ α.voc) : ∀ δ ∈ P α ℓ, x ∉ δ.pvoc := by
   intro δ δ_in
   cases α
   all_goals
-    simp_all [P, voc, vocabOfFormula, vocabOfProgram, Vocab.fromList]
+    simp_all [P, Formula.voc, Program.voc, Vocab.fromList]
   case test τ =>
-    cases em (ℓ ⟨τ, by simp [testsOfProgram]⟩) <;> simp_all [vocabOfFormula, Vocab.fromList]
+    cases em (ℓ ⟨τ, by simp [testsOfProgram]⟩) <;> simp_all [Formula.voc, Vocab.fromList]
   case sequence α β =>
     have IHα := keepFreshP α ℓ x_notin.1
     have IHβ := keepFreshP β ℓ x_notin.2
-    simp_all [P, voc, vocabOfFormula, vocabOfProgram, Vocab.fromList, List.mem_filter, Vocab.fromListProgram_map_iff]
+    simp_all [P, Formula.voc, Program.voc, Vocab.fromList, List.mem_filter, Vocab.fromListProgram_map_iff]
     rcases δ_in with (⟨δ', δ'_in, def_δ⟩ | δ_in)
     · subst def_δ
       have := IHα _ δ'_in.1
@@ -359,30 +357,35 @@ theorem keepFreshP α ℓ (x_notin : x ∉ voc α) : ∀ δ ∈ P α ℓ, x ∉
   case union α β =>
     have IHα := keepFreshP α ℓ x_notin.1
     have IHβ := keepFreshP β ℓ x_notin.2
-    simp_all [P, voc, vocabOfFormula, vocabOfProgram, Vocab.fromList, List.mem_filter]
+    simp_all [P, Formula.voc, Program.voc, Vocab.fromList, List.mem_filter]
     aesop
   case star α =>
     have IHα := keepFreshP α ℓ x_notin
     rcases δ_in with (_ | ⟨δ', δ'_in, def_δ⟩)
     · subst_eqs
-      simp_all [voc, Vocab.fromList, Finset.not_mem_empty, not_false_eq_true]
+      simp_all [Vocab.fromList, Finset.not_mem_empty, not_false_eq_true]
     · subst def_δ
       rw [Vocab.fromListProgram_map_iff]
-      simp_all [voc, Vocab.fromList, Finset.not_mem_empty, not_false_eq_true]
+      simp_all [Vocab.fromList, Finset.not_mem_empty, not_false_eq_true]
       rintro γ (γ_in_δ' | γ_def)
       · have := IHα _ δ'_in.1
         simp_all [Vocab.fromListProgram_map_iff]
       · subst γ_def
-        simp [vocabOfProgram]
+        simp [Program.voc]
         aesop
 
-/-- Depending on α we know what can occur inside `δ ∈ P α ℓ` for unfoldBox.
-The notes also say `δ1n ⊆ progsOf α \ {α}` but we do not include this here yet. -/
+/-- Depending on α we know what can occur inside `δ ∈ P α ℓ` for unfoldBox. -/
 theorem boxHelperTermination α (ℓ : TP α) :
   ∀ δ ∈ P α ℓ,
       ( α.isAtomic → δ = [α] )
-    ∧ ( ∀ β, α = (∗β) → δ = [] ∨ ∃ a, ∃ δ1n, δ = [(·a : Program)] ++ δ1n ++ [∗β] )
-    ∧ ( (¬ α.isAtomic ∧ ¬ α.isStar) → δ = [] ∨ ∃ a, ∃ δ1n, δ = [(·a : Program)] ++ δ1n )
+    ∧ ( ∀ β, α = (∗β) →
+          δ = []
+        ∨ ∃ a δ1n, (δ = [(·a : Program)] ++ δ1n ++ [∗β]
+                    ∧ ((·a : Program)::δ) ⊆ subprograms α) )
+    ∧ ( (¬ α.isAtomic ∧ ¬ α.isStar) →
+          δ = []
+        ∨ ∃ a δ1n, (δ = [(·a : Program)] ++ δ1n
+                    ∧ ((·a : Program)::δ) ⊆ subprograms α) )
     := by
   intro δ δ_in
   cases α
@@ -404,20 +407,33 @@ theorem boxHelperTermination α (ℓ : TP α) :
         rename _ => hyp2
         rcases hyp2 with ⟨a, α_def⟩
         cases α_def
-      · rw [Program.isAtomic_iff] at *
-        simp_all
+      case neg isAt notStar =>
+        rw [Program.isAtomic_iff] at isAt
+        rcases isAt with ⟨a, α_def⟩
+        use a
+        subst α_def
+        simp [subprograms]
       · rw [Program.isStar_iff] at *
         rename _ => hyp
         rcases hyp with ⟨γ, α_def⟩
         specialize IH γ
-        simp_all
-        rcases IH with ⟨a, δ1n, δ'_def⟩
+        simp_all [subprograms]
+        rcases IH with ⟨a, ⟨δ1n, δ'_def⟩, ⟨a_in, δ'_sub⟩⟩
+        use a
         subst δ'_def
-        simp
-      · rcases IH.2 with ⟨a, δ1n, δ'_def⟩
-        simp_all
+        simp at *
+        constructor
+        · left; exact a_in
+        · subst α_def
+          intro α α_in
+          have := δ'_sub.2 α_in
+          aesop
+      · rcases IH.2 with ⟨a, ⟨δ1n, δ'_def⟩, ⟨_, δ'_sub⟩⟩
+        subst δ'_def
+        simp [subprograms] at *
+        aesop
     · by_cases [] ∈ P α ℓ
-      · simp_all
+      · simp_all [subprograms]
         have IH := boxHelperTermination β ℓ δ δ_in
         simp_all
         by_cases β.isAtomic <;> by_cases β.isStar <;> simp_all
@@ -431,46 +447,64 @@ theorem boxHelperTermination α (ℓ : TP α) :
           rcases hyp2 with ⟨a, α_def⟩
           cases α_def
         · rw [Program.isAtomic_iff] at *
-          simp_all
+          cases IH
+          subst_eqs
+          simp_all [subprograms]
+          aesop
         · rw [Program.isStar_iff] at *
           rename _ => hyp
           rcases hyp with ⟨γ, α_def⟩
           specialize IH γ
           simp_all
           rcases IH with ⟨a, δ1n, δ'_def⟩ <;> aesop
+        · cases IH
+          simp_all [subprograms]
+          aesop
       · simp_all
   case union α β =>
     cases δ_in
     case inl δ_in =>
-      have IH := boxHelperTermination α ℓ δ δ_in
-      cases em α.isAtomic <;> cases em α.isStar <;> simp_all
-      all_goals
-        rw [Program.isAtomic_iff] at *
-        rw [Program.isStar_iff] at *
-        simp_all
-      · rename _ => hyp
-        rcases hyp with ⟨γ, α_def⟩
-        specialize IH γ
+      by_cases α.isAtomic <;> by_cases α.isStar <;>
+        simp_all [Program.isAtomic_iff, Program.isStar_iff, subprograms]
+      case pos hyp1 hyp2 =>
+        rcases hyp1 with ⟨γ, α_def⟩
+        rcases hyp2 with ⟨γ, α_def⟩
+        subst_eqs
+      case pos hyp1 hyp2 =>
+        rcases hyp2 with ⟨γ, α_def⟩
+        subst α_def
         simp_all
-        rcases IH with _ | ⟨a, δ1n, bla ⟩
-        · left; assumption
-        · right
-          use a, δ1n ++ [∗γ]
+        have IH := boxHelperTermination (∗γ) ℓ δ δ_in
+        aesop
+      case neg hyp1 hyp2 =>
+        rcases hyp1 with ⟨a, α_def⟩
+        subst α_def
+        have IH := boxHelperTermination (·a : Program) ℓ δ δ_in
+        simp_all [Program.isAtomic_iff, Program.isStar_iff, subprograms]
+      · have IH := boxHelperTermination (α) ℓ δ δ_in
+        simp_all [Program.isAtomic_iff, Program.isStar_iff, subprograms]
+        aesop
     case inr δ_in =>
-      have IH := boxHelperTermination β ℓ δ δ_in
-      cases em β.isAtomic <;> cases em β.isStar <;> simp_all
-      all_goals
-        try rw [Program.isAtomic_iff] at *
-        try simp_all
-      · try rw [Program.isStar_iff] at *
-        rename _ => hyp
-        rcases hyp with ⟨γ, α_def⟩
-        specialize IH γ
+      by_cases β.isAtomic <;> by_cases β.isStar <;>
+        simp_all [Program.isAtomic_iff, Program.isStar_iff, subprograms]
+      case pos hyp1 hyp2 =>
+        rcases hyp1 with ⟨γ, β_def⟩
+        rcases hyp2 with ⟨γ, β_def⟩
+        subst_eqs
+      case pos hyp1 hyp2 =>
+        rcases hyp2 with ⟨γ, β_def⟩
+        subst β_def
         simp_all
-        rcases IH with _ | ⟨a, δ1n, _⟩
-        · left; assumption
-        · right
-          use a, δ1n ++ [∗γ]
+        have IH := boxHelperTermination (∗γ) ℓ δ δ_in
+        aesop
+      case neg hyp1 hyp2 =>
+        rcases hyp1 with ⟨a, β_def⟩
+        subst β_def
+        have IH := boxHelperTermination (·a : Program) ℓ δ δ_in
+        simp_all [Program.isAtomic_iff, Program.isStar_iff, subprograms]
+      · have IH := boxHelperTermination (β) ℓ δ δ_in
+        simp_all [Program.isAtomic_iff, Program.isStar_iff, subprograms]
+        aesop
   case test τ =>
     cases em (ℓ ⟨τ, by simp [testsOfProgram]⟩)
     · simp_all
@@ -485,25 +519,38 @@ theorem boxHelperTermination α (ℓ : TP α) :
       have IH := boxHelperTermination β ℓ δ' δ'_in
       cases em β.isAtomic <;> cases em β.isStar <;> simp_all
       all_goals
-        try rw [Program.isAtomic_iff] at *
-        try simp_all
-      · try rw [Program.isStar_iff] at *
-        rename _ => hyp
-        rcases hyp with ⟨γ, α_def⟩
-        specialize IH γ α_def
-        simp_all only [not_false_eq_true, implies_true]
-        rcases IH with ⟨a, δ1n, δ'_def⟩
+        simp_all [Program.isAtomic_iff, Program.isStar_iff]
+      · rename _ => hyp
+        rcases hyp with ⟨γ, β_def⟩
+        subst β_def
+        have := IH.2 γ rfl
+        simp_all [not_false_eq_true, implies_true]
+      · rename ∃ a, β = (·a : Program) => hyp
+        rcases hyp with ⟨a, β_def⟩
+        subst β_def
+        simp [subprograms]
+      · rename ∃ α, β = (∗α) => hyp
+        rcases hyp with ⟨α, β_def⟩
+        subst β_def
+        specialize IH α rfl
+        simp [subprograms] at *
+        rcases IH with ⟨a, ⟨δ1n, δ'_def⟩, ⟨a_in, δ'_sub⟩⟩
+        use a
+        constructor
+        · use δ1n ++ [∗ α]
+          subst δ'_def
+          simp
+        · aesop
+      · rcases IH with ⟨a, ⟨δ1n, δ'_def⟩, ⟨a_in, δ'_sub⟩⟩
         subst δ'_def
-        simp_all
-        use δ1n ++ [∗γ]
-        simp
-      · rcases IH.2 with ⟨a, δ1n, δ'_def⟩
-        simp_all
+        use a
+        constructor
+        · use δ1n
+          simp
+        · simp_all [subprograms]
 
 /-- Where formulas in the unfolding can come from.
-NOTE: the paper version says two things more which we omit here:
- - `φ ∈ fischerLadner [⌈α⌉ψ]`
- - `∀ γ ∈ (a::δ), γ ∈ subprograms α` (in the last conjunct) -/
+NOTE: the paper version also says `φ ∈ fischerLadner [⌈α⌉ψ]` which we omit here. -/
 theorem unfoldBoxContent α ψ :
     ∀ X ∈ (unfoldBox α ψ),
     ∀ φ ∈ X,
@@ -511,7 +558,7 @@ theorem unfoldBoxContent α ψ :
         -- ∧
         (  (φ = ψ)
          ∨ (∃ τ ∈ testsOfProgram α, φ = (~τ))
-         ∨ (∃ (a : Nat), ∃ δ, φ = (⌈·a⌉⌈⌈δ⌉⌉ψ) /- ∧ ∀ γ ∈ (a::δ), γ ∈ subprograms α -/))
+         ∨ (∃ (a : Nat), ∃ δ, φ = (⌈·a⌉⌈⌈δ⌉⌉ψ) ∧ ∀ γ ∈ ((·a : Program)::δ), γ ∈ subprograms α))
     := by
   intro X X_in φ φ_in_X
   simp [unfoldBox, Xset] at X_in
@@ -548,32 +595,49 @@ theorem unfoldBoxContent α ψ :
       case atom_prog a =>
         clear bht
         right
+        use a
         use []
         simp
       case sequence α β =>
-        rcases bht with _ | ⟨a, δ1n, δ_def⟩
+        rcases bht with _ | ⟨a, ⟨δ1n, δ_def⟩, ⟨a_in, δ_sub⟩⟩
         · subst_eqs; simp
         · subst δ_def
-          simp_all
+          simp_all -- FIXME: `simp_all?` gives wrong suggestion?
           right
+          use a
           use δ1n
+          simp_all [subprograms]
+          intro γ γ_in
+          specialize δ_sub γ_in
+          simp_all
       case union α β =>
-        rcases bht with _ | ⟨a, δ1n, δ_def⟩
+        rcases bht with _ | ⟨a, ⟨δ1n, δ_def⟩, ⟨a_in, δ_sub⟩⟩
         · subst_eqs; simp
         · subst δ_def
-          simp_all
+          simp_all -- FIXME: `simp_all?` gives wrong suggestion?
           right
-          use δ1n
+          use a, δ1n
+          simp
+          constructor
+          · assumption
+          · intro γ γ_in
+            specialize δ_sub γ_in
+            simp_all
       case star β =>
-        rcases bht with _ | ⟨a, δ1n, δ_def⟩
+        rcases bht with _ | ⟨a, ⟨δ1n, δ_def⟩, ⟨a_in, δ_sub⟩⟩
         · subst_eqs; simp
         · subst δ_def
           simp_all
           right
-          use δ1n ++ [∗β]
-      case test τ =>
-        simp only [allTP, List.mem_map, List.mem_sublists] at *
-        by_cases ℓ ⟨τ, (by simp : τ ∈ [τ])⟩ <;> simp_all
+          use a, δ1n ++ [∗β]
+          simp
+          constructor
+          · assumption
+          · intro γ γ_in
+            rcases γ_in with γ_in | γ_in
+            · specialize δ_sub γ_in
+              aesop
+            · aesop
 
 theorem boxHelperTP α (ℓ : TP α) :
     (∀ τ, (~τ.val) ∈ F α ℓ → ℓ τ = false)
@@ -611,7 +675,7 @@ theorem boxHelperTP α (ℓ : TP α) :
       · aesop
 
 theorem guardToStar (x : Nat) β χ0 χ1 ρ ψ
-    (x_notin_beta : Sum.inl x ∉ HasVocabulary.voc β)
+    (x_notin_beta : Sum.inl x ∉ β.voc)
     (beta_equiv : (⌈β⌉·x) ≡ (((·x) ⋀ χ0) ⋁ χ1))
     (rho_imp_repl : ρ ⊨ (repl_in_F x ρ) (χ0 ⋁ χ1))
     (rho_imp_psi : ρ ⊨ ψ)
@@ -1061,7 +1125,7 @@ theorem localBoxTruthI γ ψ (ℓ :TP γ) :
       exact left_to_right
     · -- Right to left, "more work is required"
       let x : Nat := freshVarProg β
-      have x_not_in_β : Sum.inl x ∉ HasVocabulary.voc β := by apply freshVarProg_is_fresh
+      have x_not_in_β : Sum.inl x ∉ β.voc := by apply freshVarProg_is_fresh
       let φ ℓ := Con ((P β ℓ).map (fun αs => ⌈⌈αs⌉⌉·x))
       let T0 := (allTP β).filter (fun ℓ => [] ∈ P β ℓ)
       let T1 := (allTP β).filter (fun ℓ => [] ∉ P β ℓ)
diff --git a/Pdl/UnfoldDia.lean b/Pdl/UnfoldDia.lean
index 1e53380..615e5ee 100644
--- a/Pdl/UnfoldDia.lean
+++ b/Pdl/UnfoldDia.lean
@@ -6,8 +6,6 @@ import Pdl.Substitution
 import Pdl.Fresh
 import Pdl.Star
 
-open HasVocabulary
-
 -- ### Diamonds: H, Y and Φ_⋄
 
 def H : Program → List (List Formula × List Program)
@@ -117,15 +115,15 @@ theorem H_mem_sequence α {Fs δ} (in_H : ⟨Fs, δ⟩ ∈ H α) :
   case test τ =>
     simp_all [H]
 
-theorem keepFreshH α : x ∉ voc α → ∀ F δ, (F,δ) ∈ H α → x ∉ voc F ∧ x ∉ voc δ := by
+theorem keepFreshH α : x ∉ α.voc → ∀ F δ, (F,δ) ∈ H α → x ∉ F.fvoc ∧ x ∉ δ.pvoc := by
   intro x_notin F δ Fδ_in_H
   cases α
   all_goals
-    simp [H, voc, vocabOfFormula, vocabOfProgram, Vocab.fromList] at *
+    simp [H, Formula.voc, Program.voc, Vocab.fromList] at *
   case atom_prog a =>
     cases Fδ_in_H
     subst_eqs
-    simp [vocabOfProgram, Vocab.fromList]
+    simp [Program.voc, Vocab.fromList]
     assumption
   case test =>
     cases Fδ_in_H
@@ -140,7 +138,7 @@ theorem keepFreshH α : x ∉ voc α → ∀ F δ, (F,δ) ∈ H α → x ∉ voc
     cases em (δ' = []) <;> simp_all
     · subst_eqs
       have IHα := keepFreshH α x_notin.1 F' [] Fδ'_in
-      simp_all [H, voc, vocabOfFormula, vocabOfProgram, Vocab.fromList]
+      simp_all [H, Formula.voc, Program.voc, Vocab.fromList]
       rcases Fδ_in_l with ⟨l', ⟨⟨a', b', ⟨a'b'_in_Hβ, def_l'⟩⟩, Fδ_in_l'⟩⟩
       subst_eqs
       simp_all [Vocab.fromListFormula_map_iff]
@@ -149,16 +147,16 @@ theorem keepFreshH α : x ∉ voc α → ∀ F δ, (F,δ) ∈ H α → x ∉ voc
       · apply IHα
         assumption
       · have IHβ := keepFreshH β x_notin.2 a' b' a'b'_in_Hβ
-        simp_all [H, voc, vocabOfFormula, vocabOfProgram, Vocab.fromListFormula_map_iff]
+        simp_all [H, Formula.voc, Program.voc, Vocab.fromListFormula_map_iff]
     · have := keepFreshH α x_notin.1 F' δ' Fδ'_in
-      simp_all [H, voc,vocabOfFormula,vocabOfProgram]
+      simp_all [H, Formula.voc, Program.voc]
   case sequence.right α β =>
     rcases Fδ_in_H with ⟨l, ⟨⟨F', δ', ⟨Fδ'_in, def_l⟩⟩, Fδ_in_l⟩⟩
     subst def_l
     cases em (δ' = []) <;> simp_all
     · subst_eqs
       have IHα := keepFreshH α x_notin.1 F' [] Fδ'_in
-      simp_all [H, voc, vocabOfFormula, vocabOfProgram, Vocab.fromList]
+      simp_all [H, Formula.voc, Program.voc, Vocab.fromList]
       rcases Fδ_in_l with ⟨l', ⟨⟨a', b', ⟨a'b'_in_Hβ, def_l'⟩⟩, Fδ_in_l'⟩⟩
       subst_eqs
       simp_all
@@ -233,7 +231,7 @@ theorem unfoldDiamondContent α ψ :
     aesop
 
 theorem guardToStarDiamond (x : Nat)
-    (x_notin_beta : Sum.inl x ∉ HasVocabulary.voc β)
+    (x_notin_beta : Sum.inl x ∉ β.voc)
     (beta_equiv : (~⌈β⌉~·x) ≡ (((·x) ⋀ σ0) ⋁ σ1))
     (repl_imp_rho : repl_in_F x ρ σ1 ⊨ ρ)
     (notPsi_imp_rho : (~ψ) ⊨ ρ)
@@ -464,7 +462,7 @@ theorem localDiamondTruth γ ψ : (~⌈γ⌉ψ) ≡ dis ( (H γ).map (fun Fδ =>
       -- An alternative idea to solve this would have been to refactor everything
       -- to allow different types, but that seemed harder and not (yet?!) needed.
       let x : Nat := freshVarProg β
-      have x_not_in : Sum.inl x ∉ HasVocabulary.voc β := by apply freshVarProg_is_fresh
+      have x_not_in : Sum.inl x ∉ β.voc := by apply freshVarProg_is_fresh
       -- NOTE the use of ⊥ below - matters for rhs-to-lhs in first Lemma condition.
       let σ0 : Formula := dis $
         (H β).map (fun (F,δ) => if δ = [] then Con F else ⊥)
diff --git a/Pdl/Vocab.lean b/Pdl/Vocab.lean
index 2b373e2..830b405 100644
--- a/Pdl/Vocab.lean
+++ b/Pdl/Vocab.lean
@@ -14,33 +14,21 @@ def Vocab.atomProgs : Vocab → Finset Nat :=
 
 mutual
   @[simp]
-  def vocabOfProgram : Program → Vocab
+  def Program.voc : Program → Vocab
     | ·n => {.inr n}
-    | α;'β => vocabOfProgram α ∪ vocabOfProgram β
-    | α ⋓ β => vocabOfProgram α ∪ vocabOfProgram β
-    | ∗α => vocabOfProgram α
-    | ?' φ => vocabOfFormula φ
+    | α;'β => α.voc ∪ β.voc
+    | α ⋓ β => α.voc ∪ β.voc
+    | ∗α => α.voc
+    | ?' φ => φ.voc
   @[simp]
-  def vocabOfFormula : Formula → Vocab
+  def Formula.voc : Formula → Vocab
     | ⊥ => ∅
     | ·n => {.inl n}
-    | ~φ => vocabOfFormula φ
-    | φ⋀ψ => vocabOfFormula φ ∪ vocabOfFormula ψ
-    | ⌈α⌉ φ => vocabOfProgram α ∪ vocabOfFormula φ
+    | ~φ => φ.voc
+    | φ⋀ψ => φ.voc ∪ ψ.voc
+    | ⌈α⌉ φ => α.voc ∪ φ.voc
 end
 
--- avoid this, instead rename the above to Formula.voc and Program.voc ?
-class HasVocabulary (α : Type) where
-  voc : α → Vocab
-
-open HasVocabulary
-
-@[simp]
-instance formulaHasVocabulary : HasVocabulary Formula := ⟨vocabOfFormula⟩
-
-@[simp]
-instance programHasVocabulary : HasVocabulary Program := ⟨vocabOfProgram⟩
-
 -- rename to Vocab.join? or use `class Hadd`?
 -- QUESTION: Is there a List.join but for Finset?
 @[simp]
@@ -48,6 +36,12 @@ def Vocab.fromList : (L : List Vocab) → Vocab
 | [] => {}
 | (v::vs) => v ∪ Vocab.fromList vs
 
+@[simp]
+abbrev List.fvoc (L : List Formula) := Vocab.fromList (L.map Formula.voc)
+
+@[simp]
+abbrev List.pvoc (L : List Program) := Vocab.fromList (L.map Program.voc)
+
 @[simp]
 theorem Vocab.fromList_singleton : Vocab.fromList [V] = V := by
   simp [Vocab.fromList]
@@ -56,17 +50,9 @@ theorem Vocab.fromList_singleton : Vocab.fromList [V] = V := by
 theorem Vocab.fromList_append : Vocab.fromList (L ++ R) = Vocab.fromList L ∪ Vocab.fromList R := by
   induction L <;> induction R <;> simp_all
 
-@[simp]
-instance [HasVocabulary α] : HasVocabulary (List α) :=
-  ⟨fun X => .fromList (X.map voc)⟩
-
--- delete this?
-instance [HasVocabulary α] : HasVocabulary (Finset α) :=
-  ⟨fun X => (X.biUnion (fun f => {voc f})).fold (fun x y => x ∪ y) {} id⟩
-
 theorem Vocab.fromListFormula_map_iff n (L : List Formula) :
-    n ∈ Vocab.fromList (L.map vocabOfFormula)
-    ↔ ∃ φ ∈ L, n ∈ vocabOfFormula φ := by
+    n ∈ Vocab.fromList (L.map Formula.voc)
+    ↔ ∃ φ ∈ L, n ∈ Formula.voc φ := by
   induction L
   · simp [fromList]
   case cons h t IH =>
@@ -82,27 +68,11 @@ theorem Vocab.fromListProgram_map_iff n (L : List Program) :
     simp only [fromList, Finset.mem_union, List.mem_cons, exists_eq_or_imp]
     rw [← IH]
 
-theorem inVocList {α} [HasVocabulary α] n (L : List α) :
-    n ∈ voc L
-    ↔ ∃ φ ∈ L, n ∈ voc φ := by
-  induction L
-  · simp [voc, Finset.mem_biUnion, List.mem_toFinset, Vocab.fromList]
-  case cons h t IH =>
-    simp only [voc, Vocab.fromList, Finset.mem_union, List.mem_cons, exists_eq_or_imp]
-    rw [← IH]
-    simp only [voc]
-
 @[simp]
-def vocabOfLoadFormula (lf : LoadFormula) : Vocab := vocabOfFormula (unload lf)
+def LoadFormula.voc (lf : LoadFormula) : Vocab := (unload lf).voc
 
 @[simp]
-def vocabOfNegLoadFormula (nlf : NegLoadFormula) : Vocab := vocabOfFormula (negUnload nlf)
-
-@[simp]
-instance LoadFormula.instHasVocabulary : HasVocabulary LoadFormula := ⟨vocabOfLoadFormula⟩
-
-@[simp]
-instance NegLoadFormula.instHasVocabulary : HasVocabulary NegLoadFormula := ⟨vocabOfNegLoadFormula⟩
+def NegLoadFormula.voc (nlf : NegLoadFormula) : Vocab := (negUnload nlf).voc
 
 /-- Test(α) -/
 def testsOfProgram : Program → List Formula
@@ -119,3 +89,30 @@ def subprograms : Program → List Program
 | α;'β => [α;'β ] ++ subprograms α ++ subprograms β
 | α ⋓ β => [α ⋓ β] ++ subprograms α ++ subprograms β
 | ∗α => [∗α] ++ subprograms α
+
+@[simp]
+theorem subprograms.refl : α ∈ subprograms α := by
+  cases α <;> simp [subprograms]
+
+theorem testsOfProgram.voc α {τ} (τ_in : τ ∈ testsOfProgram α) : τ.voc ⊆ α.voc := by
+  cases α <;> simp_all [testsOfProgram]
+  case sequence α β =>
+    intro x x_in
+    rcases τ_in with hyp | hyp
+    all_goals
+      have := testsOfProgram.voc _ hyp
+      specialize this x_in
+      simp only [Finset.mem_union]
+      tauto
+  case union α β =>
+    intro x x_in
+    rcases τ_in with hyp | hyp
+    all_goals
+      have := testsOfProgram.voc _ hyp
+      specialize this x_in
+      simp only [Finset.mem_union]
+      tauto
+  case star α =>
+    intro x x_in
+    have := testsOfProgram.voc _ τ_in
+    exact this x_in