specialize this (freshVarProg α)
α : Program
this : ∀ n ∈ vocabOfProgram α, n < freshVarProg α
hyp : freshVarProg α ∈ vocabOfProgram α
⊢ False
α : Program
hyp : freshVarProg α ∈ vocabOfProgram α
this : freshVarProg α ∈ vocabOfProgram α → freshVarProg α < freshVarProg α
⊢ False