cases Fδ_in_l
case intro.intro.intro.intro.intro.inr
x : ℕ
F : List Formula
δ : List Program
α : Program
x_notin : x ∉ vocabOfProgram α
y : Program
F' : List Formula
δ' : List Program
y_in : y ∈ δ' ∨ y = (∗α)
Fδ'_in_Hα : (F', δ') ∈ H α
Fδ_in_l : F = F' ∧ δ = δ' ++ [∗α]
IHα : (∀ x_1 ∈ F', x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ δ', x ∉ vocabOfProgram x_1
h✝ : ¬δ' = []
⊢ x ∉ vocabOfProgram y
case intro.intro.intro.intro.intro.inr.intro
x : ℕ
F : List Formula
δ : List Program
α : Program
x_notin : x ∉ vocabOfProgram α
y : Program
F' : List Formula
δ' : List Program
y_in : y ∈ δ' ∨ y = (∗α)
Fδ'_in_Hα : (F', δ') ∈ H α
IHα : (∀ x_1 ∈ F', x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ δ', x ∉ vocabOfProgram x_1
h✝ : ¬δ' = []
left✝ : F = F'
right✝ : δ = δ' ++ [∗α]
⊢ x ∉ vocabOfProgram y