Comment by kaashif

The fact that you have found a function of type () -> () is a proof that true implies true. This is the Curry-Howard isomorphism.

Not a particularly interesting proof.