cases em (δ' = []) <;> simp_all
case intro.intro.intro.intro.intro
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Program
y_in : y ∈ δ
F' : List Formula
δ' : List Program
Fδ'_in : (F', δ') ∈ H α
Fδ_in_l : (F, δ) ∈ if δ' = [] then (List.map (fun x => [(F' ∪ x.1, x.2)]) (H β)).join else [(F', δ' ++ [β])]
⊢ x ∉ vocabOfProgram y
case intro.intro.intro.intro.intro.inl
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Program
y_in : y ∈ δ
F' : List Formula
δ' : List Program
Fδ'_in : (F', []) ∈ H α
Fδ_in_l : ∃ l, (∃ a b, (a, b) ∈ H β ∧ [(F' ∪ a, b)] = l) ∧ (F, δ) ∈ l
h✝ : δ' = []
⊢ x ∉ vocabOfProgram y

case intro.intro.intro.intro.intro.inr
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Program
F' : List Formula
δ' : List Program
y_in : y ∈ δ' ∨ y = β
Fδ'_in : (F', δ') ∈ H α
Fδ_in_l : F = F' ∧ δ = δ' ++ [β]
h✝ : ¬δ' = []
⊢ x ∉ vocabOfProgram y