proposition: Lemma map_bind : forall A B C (f : B -> C) (m:M A) g, (f <$> bind m g = bind m (fun x => f <$> (g x))).
proof: Proof. intros ; cbv. rewrite monad_law3. reflexivity. Qed.
imports: Coq(ssreflect ssrfun FunctionalExtensionality) Mon(SPropBase) Coq(Relation_Definitions Morphisms)