clear IH
case right
x : ℕ
ψ : Formula
α : Program
δ : List Program
IH : x ∉ voc δ → repl_in_F x ψ (⌈⌈δ⌉⌉~·x) = ⌈⌈δ⌉⌉~ψ
nonOcc : x ∉ voc (α :: δ)
⊢ x ∉ voc δ
case right
x : ℕ
ψ : Formula
α : Program
δ : List Program
nonOcc : x ∉ voc (α :: δ)
⊢ x ∉ voc δ