fact: Definition WUpd_rel A : relation (WUpd A) := fun m1 m2 => forall p, cod_rel (proj1_sig m1 p) (proj1_sig m2 p).
imports: Coq(ssreflect) Coq(Relation_Definitions Morphisms) Mon(SPropBase SPropMonadicStructures Monoid)