You can't because the function takes three arguments: an x and y of type integer, and a "z" of type "proof that x < y". This is the "types as propositions, pro

You can't because the function takes three arguments: an x and y of type integer, and a "z" of type "proof that x < y". This is the "types as propositions, proofs as instances" Curry-Howard correspondence lightbulb: The type "x < y" is a proposition, and if you can find any z at all of that type, then z is a proof of the proposition. So by passing in such a z that has been verified to have that type, you've certified that x < y.