have := keepFreshH α x_notin F δ' Fδ'_in_Hα
case intro.intro.intro.intro.intro.inr.intro.refl.refl.inl
x : ℕ
F : List Formula
α : Program
x_notin : x ∉ vocabOfProgram α
y : Program
δ' : List Program
h✝¹ : ¬δ' = []
Fδ'_in_Hα : (F, δ') ∈ H α
IHα : (∀ x_1 ∈ F, x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ δ', x ∉ vocabOfProgram x_1
h✝ : y ∈ δ'
⊢ x ∉ vocabOfProgram y
case intro.intro.intro.intro.intro.inr.intro.refl.refl.inl
x : ℕ
F : List Formula
α : Program
x_notin : x ∉ vocabOfProgram α
y : Program
δ' : List Program
h✝¹ : ¬δ' = []
Fδ'_in_Hα : (F, δ') ∈ H α
IHα : (∀ x_1 ∈ F, x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ δ', x ∉ vocabOfProgram x_1
h✝ : y ∈ δ'
this : x ∉ voc F ∧ x ∉ voc δ'
⊢ x ∉ vocabOfProgram y