case test =>
  cases Fδ_in_H
  subst_eqs
  aesop
x : ℕ
F : List Formula
δ : List Program
a✝ : Formula
x_notin : x ∉ vocabOfFormula a✝
Fδ_in_H : F = [a✝] ∧ δ = []
⊢ (∀ x_1 ∈ F, x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ δ, x ∉ vocabOfProgram x_1
no goals