fact: Definition points (X:Rel) : Type := { p : πl X × πr X ⫳ X (nfst p) (nsnd p)}.
imports: Coq(ssreflect ssrfun ssrbool) Coq(Relation_Definitions Morphisms) Mon(SPropBase) Relational(Category RelativeMonads EnrichedSetting)