fact: Record RelationalSpecMonad := mkRSM { rsm_left : unarySpecMonad ; rsm_right : unarySpecMonad ; rsm_rel : rsm_components rsm_left rsm_right }.
imports: Coq(ssreflect ssrfun ssrbool) Coq(FunctionalExtensionality) Coq(Relation_Definitions Morphisms RelationPairs) Mon(SPropBase SPropMonadicStructures) Relational(OrderEnrichedCategory Rel)