cases φ
φ : Formula
⊢ ∀ n ∈ voc φ, n < freshVarForm φ
case bottom

⊢ ∀ n ∈ voc Formula.bottom, n < freshVarForm Formula.bottom

case atom_prop
a✝ : ℕ
⊢ ∀ n ∈ voc (·a✝), n < freshVarForm (·a✝)

case neg
a✝ : Formula
⊢ ∀ n ∈ voc (~a✝), n < freshVarForm (~a✝)

case and
a✝¹ a✝ : Formula
⊢ ∀ n ∈ voc (a✝¹⋀a✝), n < freshVarForm (a✝¹⋀a✝)

case box
a✝¹ : Program
a✝ : Formula
⊢ ∀ n ∈ voc (⌈a✝¹⌉a✝), n < freshVarForm (⌈a✝¹⌉a✝)