by_contra hyp
α : Program
this : ∀ n ∈ vocabOfProgram α, n < freshVarProg α
⊢ freshVarProg α ∉ vocabOfProgram α
α : Program
this : ∀ n ∈ vocabOfProgram α, n < freshVarProg α
hyp : freshVarProg α ∈ vocabOfProgram α
⊢ False