fact: Definition directed_property {P} (C : Directed_family P) : isdirected C := pr2 (pr2 C).
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Combinatorics.WellOrderedSets UniMath.OrderTheory.DCPOs.AlternativeDefinitions.Dcpo