all_goals simp [freshVarProg, voc, vocabOfProgram]
case atom_prog
a✝ : ℕ
⊢ ∀ n ∈ voc (·a✝), n < freshVarProg (·a✝)

case sequence
a✝¹ a✝ : Program
⊢ ∀ n ∈ voc (a✝¹;'a✝), n < freshVarProg (a✝¹;'a✝)

case union
a✝¹ a✝ : Program
⊢ ∀ n ∈ voc (a✝¹⋓a✝), n < freshVarProg (a✝¹⋓a✝)

case star
a✝ : Program
⊢ ∀ n ∈ voc (∗a✝), n < freshVarProg (∗a✝)

case test
a✝ : Formula
⊢ ∀ n ∈ voc (?'a✝), n < freshVarProg (?'a✝)
case sequence
a✝¹ a✝ : Program
⊢ ∀ (n : ℕ), n ∈ vocabOfProgram a✝¹ ∨ n ∈ vocabOfProgram a✝ → n < freshVarProg a✝¹ ∨ n < freshVarProg a✝

case union
a✝¹ a✝ : Program
⊢ ∀ (n : ℕ), n ∈ vocabOfProgram a✝¹ ∨ n ∈ vocabOfProgram a✝ → n < freshVarProg a✝¹ ∨ n < freshVarProg a✝

case star
a✝ : Program
⊢ ∀ n ∈ vocabOfProgram a✝, n < freshVarProg a✝

case test
a✝ : Formula
⊢ ∀ n ∈ vocabOfFormula a✝, n < freshVarForm a✝