fact: Record MonadIdeal : Type := mkMonadIdeal { mid_rel :> MonadRelation M W ; mid_upper_closed : forall A, Proper (pointwise_relation (M A) (@omon_rel W A ==> SProp_order)) (@mid_rel A) }.
imports: Coq(ssreflect ssrfun FunctionalExtensionality) Mon(SPropBase) Coq(Relation_Definitions Morphisms)