cases Fδ_in_H
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
Fδ_in_H : (F, δ) ∈ H α ∨ (F, δ) ∈ H β
y : Formula
y_in : y ∈ F
⊢ x ∉ vocabOfFormula y
case inl
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Formula
y_in : y ∈ F
h✝ : (F, δ) ∈ H α
⊢ x ∉ vocabOfFormula y

case inr
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Formula
y_in : y ∈ F
h✝ : (F, δ) ∈ H β
⊢ x ∉ vocabOfFormula y