Definition OrderedSet_isrefl {X:OrderedSet} (x:X) : x ≤ x. Proof. intros. unwrap_OrderedSet X; simpl in x. apply refl. Defined.
Require Import UniMath.Combinatorics.FiniteSets. Require Import UniMath.Foundations.UnivalenceAxiom. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.OrderTheory.Posets.Examples.StandardFiniteSet.