fact: Definition OrderedSet_isrefl {X:OrderedSet} (x:X) : x ≤ x.
imports: UniMath.Combinatorics.FiniteSets UniMath.Foundations.UnivalenceAxiom UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions