fact: Record MonadRelation (M W : Monad) : Type := mkMonadRelation { mrel :> forall A, M A -> W A -> Prop ; mrel_ret : forall A (a:A), mrel (ret a) (ret a) ; mrel_bind : forall A B m w (f : A -> M B) g, mrel m w -> (forall a, mrel (f a) (g a)) -> mrel (bind m f) (bind w g) }.
imports: Coq(ssreflect ssrfun FunctionalExtensionality) Mon(SPropBase) Coq(Relation_Definitions Morphisms)