have := Nat.lt_irrefl (freshVarProg α)
α : Program
hyp : freshVarProg α ∈ vocabOfProgram α
this : freshVarProg α ∈ vocabOfProgram α → freshVarProg α < freshVarProg α
⊢ False
α : Program
hyp : freshVarProg α ∈ vocabOfProgram α
this✝ : freshVarProg α ∈ vocabOfProgram α → freshVarProg α < freshVarProg α
this : ¬freshVarProg α < freshVarProg α
⊢ False