rcases hyp with ⟨l, ⟨⟨F', δ', ⟨Fδ'_in_Hα, def_l⟩⟩, Fδ_in_l⟩⟩
x : ℕ
F : List Formula
δ : List Program
α : Program
x_notin : x ∉ vocabOfProgram α
y : Formula
y_in : y ∈ F
hyp : ∃ l, (∃ a b, (a, b) ∈ H α ∧ (if b = [] then [] else [(a, b ++ [∗α])]) = l) ∧ (F, δ) ∈ l
⊢ x ∉ vocabOfFormula y
case intro.intro.intro.intro.intro
x : ℕ
F : List Formula
δ : List Program
α : Program
x_notin : x ∉ vocabOfProgram α
y : Formula
y_in : y ∈ F
l : List (List Formula × List Program)
Fδ_in_l : (F, δ) ∈ l
F' : List Formula
δ' : List Program
Fδ'_in_Hα : (F', δ') ∈ H α
def_l : (if δ' = [] then [] else [(F', δ' ++ [∗α])]) = l
⊢ x ∉ vocabOfFormula y