fact: Record MonadMorphism (M W : Monad) : Type := mkMorphism { mon_morph :> forall {A}, M A -> W A ; mon_morph_ret : forall A (a : A), mon_morph (ret a) = ret a ; mon_morph_bind : forall A B (m : M A) (f : A -> M B), mon_morph (bind m f) = bind (mon_morph m) (fun a => mon_morph (f a)) }.
imports: Coq(ssreflect ssrfun FunctionalExtensionality) Mon(SPropBase) Coq(Relation_Definitions Morphisms)