case and φ1 φ2 =>
  have IH1 := freshVarForm_is_larger φ1
  have IH2 := freshVarForm_is_larger φ2
  aesop
φ1 φ2 : Formula
⊢ ∀ (n : ℕ), n ∈ vocabOfFormula φ1 ∨ n ∈ vocabOfFormula φ2 → n < freshVarForm φ1 ∨ n < freshVarForm φ2
no goals