specialize this (freshVarForm φ)
φ : Formula
this : ∀ n ∈ vocabOfFormula φ, n < freshVarForm φ
hyp : freshVarForm φ ∈ vocabOfFormula φ
⊢ False
φ : Formula
hyp : freshVarForm φ ∈ vocabOfFormula φ
this : freshVarForm φ ∈ vocabOfFormula φ → freshVarForm φ < freshVarForm φ
⊢ False