cases y_in
case intro.intro.intro.intro.intro.inl.refl.intro.intro.intro.intro.intro.refl
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Formula
F' a' : List Formula
b' : List Program
y_in : y ∈ F' ∨ y ∈ a'
Fδ'_in : (F', []) ∈ H α
IHα : ∀ x_1 ∈ F', x ∉ vocabOfFormula x_1
a'b'_in_Hβ : (a', b') ∈ H β
Fδ_in_l' : F = F' ∪ a' ∧ δ = b'
⊢ x ∉ vocabOfFormula y
case intro.intro.intro.intro.intro.inl.refl.intro.intro.intro.intro.intro.refl.inl
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Formula
F' a' : List Formula
b' : List Program
Fδ'_in : (F', []) ∈ H α
IHα : ∀ x_1 ∈ F', x ∉ vocabOfFormula x_1
a'b'_in_Hβ : (a', b') ∈ H β
Fδ_in_l' : F = F' ∪ a' ∧ δ = b'
h✝ : y ∈ F'
⊢ x ∉ vocabOfFormula y

case intro.intro.intro.intro.intro.inl.refl.intro.intro.intro.intro.intro.refl.inr
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Formula
F' a' : List Formula
b' : List Program
Fδ'_in : (F', []) ∈ H α
IHα : ∀ x_1 ∈ F', x ∉ vocabOfFormula x_1
a'b'_in_Hβ : (a', b') ∈ H β
Fδ_in_l' : F = F' ∪ a' ∧ δ = b'
h✝ : y ∈ a'
⊢ x ∉ vocabOfFormula y