simp [freshVarProg, voc, vocabOfFormula] at *
α : Program
this : ∀ n ∈ voc α, n < freshVarProg α
⊢ freshVarProg α ∉ voc α
α : Program
this : ∀ n ∈ vocabOfProgram α, n < freshVarProg α
⊢ freshVarProg α ∉ vocabOfProgram α