induction δ
x : ℕ
ψ : Formula
δ : List Program
nonOcc : x ∉ voc δ
⊢ repl_in_F x ψ (⌈⌈δ⌉⌉~·x) = ⌈⌈δ⌉⌉~ψ
case nil
x : ℕ
ψ : Formula
nonOcc : x ∉ voc []
⊢ repl_in_F x ψ (⌈⌈[]⌉⌉~·x) = ⌈⌈[]⌉⌉~ψ

case cons
x : ℕ
ψ : Formula
head✝ : Program
tail✝ : List Program
tail_ih✝ : x ∉ voc tail✝ → repl_in_F x ψ (⌈⌈tail✝⌉⌉~·x) = ⌈⌈tail✝⌉⌉~ψ
nonOcc : x ∉ voc (head✝ :: tail✝)
⊢ repl_in_F x ψ (⌈⌈head✝ :: tail✝⌉⌉~·x) = ⌈⌈head✝ :: tail✝⌉⌉~ψ