rcases Fδ_in_H with ⟨l, ⟨⟨F', δ', ⟨Fδ'_in, def_l⟩⟩, Fδ_in_l⟩⟩
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
Fδ_in_H :
  ∃ l,
    (∃ a b,
        (a, b) ∈ H α ∧ (if b = [] then (List.map (fun x => [(a ∪ x.1, x.2)]) (H β)).join else [(a, b ++ [β])]) = l) ∧
      (F, δ) ∈ l
y : Formula
y_in : y ∈ F
⊢ x ∉ vocabOfFormula y
case intro.intro.intro.intro.intro
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ 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 : (F', δ') ∈ H α
def_l : (if δ' = [] then (List.map (fun x => [(F' ∪ x.1, x.2)]) (H β)).join else [(F', δ' ++ [β])]) = l
⊢ x ∉ vocabOfFormula y