have IHα := keepFreshH α x_notin.1 F' δ' Fδ'_in
case intro.intro.intro.intro.intro.inr.inl
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Program
F' : List Formula
δ' : List Program
Fδ'_in : (F', δ') ∈ H α
Fδ_in_l : F = F' ∧ δ = δ' ++ [β]
h✝¹ : ¬δ' = []
h✝ : y ∈ δ'
⊢ x ∉ vocabOfProgram y
case intro.intro.intro.intro.intro.inr.inl
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Program
F' : List Formula
δ' : List Program
Fδ'_in : (F', δ') ∈ H α
Fδ_in_l : F = F' ∧ δ = δ' ++ [β]
h✝¹ : ¬δ' = []
h✝ : y ∈ δ'
IHα : x ∉ voc F' ∧ x ∉ voc δ'
⊢ x ∉ vocabOfProgram y