Monad Laws

Standard monad laws.

I acknowledge that stdpp/base.v may not be the best home for the main typeclasses.

Thanks for the MR. But I have doubts whether we want to have this:

• I think this MR is incompatible with !555. We will have list as non-applied argument of the Lawful classes, so the universes of list will again be fixed.
• For many monads we don't have the laws up to Leibniz equality = (say listset, state, reader), but only up to some equivalence relation. This means we need to parametrize the class by Equiv and and Proper fields for the operations.