simp [voc,vocabOfProgram,vocabOfListProgram] at *
case right
x : ℕ
ψ : Formula
α : Program
δ : List Program
nonOcc : x ∉ voc (α :: δ)
⊢ x ∉ voc δ
case right
x : ℕ
ψ : Formula
α : Program
δ : List Program
nonOcc : x ∉ vocabOfProgram α ∧ ∀ x_1 ∈ δ, x ∉ vocabOfProgram x_1
⊢ ∀ x_1 ∈ δ, x ∉ vocabOfProgram x_1