[Haskell-cafe] Proving correctness