case union α β =>
  have IHα := freshVarProg_is_larger α
  have IHβ := freshVarProg_is_larger β
  aesop
α β : Program
⊢ ∀ (n : ℕ), n ∈ vocabOfProgram α ∨ n ∈ vocabOfProgram β → n < freshVarProg α ∨ n < freshVarProg β
no goals