simp_all [H, voc,vocabOfListFormula,vocabOfListProgram,vocabOfFormula,vocabOfProgram]
case intro.intro.intro.intro.intro.inl.refl.intro.intro.intro.intro.intro.refl
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Program
F' a' : List Formula
b' : List Program
y_in : y ∈ b'
Fδ'_in : (F', []) ∈ H α
IHα : ∀ x_1 ∈ F', x ∉ vocabOfFormula x_1
a'b'_in_Hβ : (a', b') ∈ H β
Fδ_in_l' : F = F' ∪ a' ∧ δ = b'
IHβ : x ∉ voc a' ∧ x ∉ voc b'
⊢ x ∉ vocabOfProgram y
no goals