fact: Definition dom_rel A : relation (A -> M -> Prop) := pointwise_relation A (pointwise_relation M SProp_op_order).
imports: Coq(ssreflect) Coq(Relation_Definitions Morphisms) Mon(SPropBase SPropMonadicStructures Monoid)