have IH1 := freshVarForm_is_larger φ1
φ1 φ2 : Formula
⊢ ∀ (n : ℕ), n ∈ vocabOfFormula φ1 ∨ n ∈ vocabOfFormula φ2 → n < freshVarForm φ1 ∨ n < freshVarForm φ2
φ1 φ2 : Formula
IH1 : ∀ n ∈ voc φ1, n < freshVarForm φ1
⊢ ∀ (n : ℕ), n ∈ vocabOfFormula φ1 ∨ n ∈ vocabOfFormula φ2 → n < freshVarForm φ1 ∨ n < freshVarForm φ2