have IHα := keepFreshH α x_notin.1 F' [] Fδ'_in
case intro.intro.intro.intro.intro.inl.refl
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Program
y_in : y ∈ δ
F' : List Formula
Fδ'_in : (F', []) ∈ H α
Fδ_in_l : ∃ l, (∃ a b, (a, b) ∈ H β ∧ [(F' ∪ a, b)] = l) ∧ (F, δ) ∈ l
⊢ x ∉ vocabOfProgram y
case intro.intro.intro.intro.intro.inl.refl
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Program
y_in : y ∈ δ
F' : List Formula
Fδ'_in : (F', []) ∈ H α
Fδ_in_l : ∃ l, (∃ a b, (a, b) ∈ H β ∧ [(F' ∪ a, b)] = l) ∧ (F, δ) ∈ l
IHα : x ∉ voc F' ∧ x ∉ voc []
⊢ x ∉ vocabOfProgram y