fact: Definition ArrRel (X Y : Rel) : Rel := ⦑ πl X -> πl Y, πr X -> πr Y | fun fl fr => forall xl xr, X xl xr -> Y (fl xl) (fr xr) | TyRel ⦒.
imports: Coq(ssreflect ssrfun ssrbool) Coq(Relation_Definitions Morphisms) Mon(SPropBase) Relational(Category RelativeMonads EnrichedSetting)