case box α φ =>
  have IHφ := freshVarForm_is_larger φ
  have IHα := freshVarProg_is_larger α
  aesop
α : Program
φ : Formula
⊢ ∀ (n : ℕ), n ∈ vocabOfProgram α ∨ n ∈ vocabOfFormula φ → n < freshVarProg α ∨ n < freshVarForm φ
no goals