[Haskell-cafe] Small proof intro