fact: Definition finitenessProperty (X:FiniteOrderedSet) : isfinite X := pr2 X.
imports: UniMath.Combinatorics.FiniteSets UniMath.Foundations.UnivalenceAxiom UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions