Formalized laws for the mtl library

• Laws for mtl classes
• Verified implementations for the common monad transformers
• Code to be as close to mtl and transformers as possible, rather than practical in Coq.

Future work

• Merge with coq-ext-lib
• Laws compatible with applicative