モナド則

http://d.hatena.ne.jp/zyxwv/20070823 のモナド則から、Haskell でよく使われるモナド則を導く予定。これって Coq が使えるんじゃないだろうか。しっかり紙でやってしまったけども。
とりあえず簡単なやつから。導出できたら随時追記。

   m * λa. unit a
=> m * unit
=> join (map unit m)
=> (join . (map unit)) m
=> id m
=> m