case inr hyp =>
  rcases hyp with ⟨l, ⟨⟨F', δ', ⟨Fδ'_in_Hα, def_l⟩⟩, Fδ_in_l⟩⟩
  subst def_l
  have IHα := keepFreshH α x_notin F' δ' Fδ'_in_Hα
  cases em (δ' = []) <;> simp_all [H, voc,vocabOfListFormula,vocabOfListProgram,vocabOfFormula,vocabOfProgram]
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
no goals