simp_all
case left.a
x : ℕ
ψ : Formula
α : Program
δ : List Program
IH : (∀ x_1 ∈ δ, x ∉ vocabOfProgram x_1) → repl_in_F x ψ (⌈⌈δ⌉⌉~·x) = ⌈⌈δ⌉⌉~ψ
nonOcc : x ∉ vocabOfProgram α ∧ ∀ x_1 ∈ δ, x ∉ vocabOfProgram x_1
a✝ : x ∈ vocabOfProgram α
⊢ False
no goals