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