simp [H, voc,vocabOfListFormula,vocabOfListProgram,vocabOfFormula,vocabOfProgram] at *
case test
x : ℕ
F : List Formula
δ : List Program
a✝ : Formula
x_notin : x ∉ voc (?'a✝)
Fδ_in_H : (F, δ) ∈ H (?'a✝)
⊢ x ∉ voc F ∧ x ∉ voc δ
case test
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