cases em (δ' = [])
case intro.intro.intro.intro.intro
x : ℕ
F : List Formula
δ : List Program
α : Program
x_notin : x ∉ vocabOfProgram α
y : Program
y_in : y ∈ δ
F' : List Formula
δ' : List Program
Fδ'_in_Hα : (F', δ') ∈ H α
Fδ_in_l : (F, δ) ∈ if δ' = [] then [] else [(F', δ' ++ [∗α])]
IHα : x ∉ voc F' ∧ x ∉ voc δ'
⊢ x ∉ vocabOfProgram y
case intro.intro.intro.intro.intro.inl
x : ℕ
F : List Formula
δ : List Program
α : Program
x_notin : x ∉ vocabOfProgram α
y : Program
y_in : y ∈ δ
F' : List Formula
δ' : List Program
Fδ'_in_Hα : (F', δ') ∈ H α
Fδ_in_l : (F, δ) ∈ if δ' = [] then [] else [(F', δ' ++ [∗α])]
IHα : x ∉ voc F' ∧ x ∉ voc δ'
h✝ : δ' = []
⊢ x ∉ vocabOfProgram y

case intro.intro.intro.intro.intro.inr
x : ℕ
F : List Formula
δ : List Program
α : Program
x_notin : x ∉ vocabOfProgram α
y : Program
y_in : y ∈ δ
F' : List Formula
δ' : List Program
Fδ'_in_Hα : (F', δ') ∈ H α
Fδ_in_l : (F, δ) ∈ if δ' = [] then [] else [(F', δ' ++ [∗α])]
IHα : x ∉ voc F' ∧ x ∉ voc δ'
h✝ : ¬δ' = []
⊢ x ∉ vocabOfProgram y