rcases Fδ_in_l with ⟨l', ⟨⟨a', b', ⟨a'b'_in_Hβ, def_l'⟩⟩, Fδ_in_l'⟩⟩
case intro.intro.intro.intro.intro.inl.refl
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Formula
y_in : y ∈ F
F' : List Formula
Fδ'_in : (F', []) ∈ H α
Fδ_in_l : ∃ l, (∃ a b, (a, b) ∈ H β ∧ [(F' ∪ a, b)] = l) ∧ (F, δ) ∈ l
IHα : ∀ x_1 ∈ F', x ∉ vocabOfFormula x_1
⊢ x ∉ vocabOfFormula y
case intro.intro.intro.intro.intro.inl.refl.intro.intro.intro.intro.intro
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Formula
y_in : y ∈ F
F' : List Formula
Fδ'_in : (F', []) ∈ H α
IHα : ∀ x_1 ∈ F', x ∉ vocabOfFormula x_1
l' : List (List Formula × List Program)
Fδ_in_l' : (F, δ) ∈ l'
a' : List Formula
b' : List Program
a'b'_in_Hβ : (a', b') ∈ H β
def_l' : [(F' ∪ a', b')] = l'
⊢ x ∉ vocabOfFormula y