by_contra hyp
φ : Formula
this : ∀ n ∈ vocabOfFormula φ, n < freshVarForm φ
⊢ freshVarForm φ ∉ vocabOfFormula φ
φ : Formula
this : ∀ n ∈ vocabOfFormula φ, n < freshVarForm φ
hyp : freshVarForm φ ∈ vocabOfFormula φ
⊢ False