Changes:
- There was a name clash in dobind, renamed one to movebind
- Added mcontests.v, currently containing
 * some simple tests
 * transitive, reflexive closure of the reduction operator
 * notations >>=, --> and -->*
 * Monadic left identity: ret a >>= f = f a in the form ret a >>= f -->*
f a

Future additions: monadic right identity, monadic associativity, fork
proprties