fact: Record relationalEffectObservation := mkREO { reo_left : unaryEffectObs M1 (rsm_left W) ; reo_right : unaryEffectObs M2 (rsm_right W) ; reo_rel : reo_components (rsm_rel W) reo_left reo_right }.
imports: Coq(ssreflect ssrfun ssrbool) Coq(FunctionalExtensionality) Coq(Relation_Definitions Morphisms RelationPairs) Mon(SPropBase SPropMonadicStructures) Relational(OrderEnrichedCategory Rel)