fact: Definition Rel : Type := { AB : Type × Type ⫳ nfst AB -> nsnd AB -> Type }.
imports: Coq(ssreflect ssrfun ssrbool) Coq(Relation_Definitions Morphisms) Mon(SPropBase) Relational(Category RelativeMonads EnrichedSetting)