have IHβ := keepFreshH β x_notin.2 F δ
case inr
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Program
y_in : y ∈ δ
h✝ : (F, δ) ∈ H β
⊢ x ∉ vocabOfProgram y
case inr
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Program
y_in : y ∈ δ
h✝ : (F, δ) ∈ H β
IHβ : (F, δ) ∈ H β → x ∉ voc F ∧ x ∉ voc δ
⊢ x ∉ vocabOfProgram y