simp [freshVarForm, voc, vocabOfFormula] at *
φ : Formula
this : ∀ n ∈ voc φ, n < freshVarForm φ
⊢ freshVarForm φ ∉ voc φ
φ : Formula
this : ∀ n ∈ vocabOfFormula φ, n < freshVarForm φ
⊢ freshVarForm φ ∉ vocabOfFormula φ