Lemma WOlt_isirrefl (X : WellOrderedSet) : isirrefl (@WOlt X). Proof. now intros x; simpl; intros H; apply H, WO_isrefl. Qed.
Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.Propositions. Require Import UniMath.MoreFoundations.Subtypes. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.AxiomOfChoice. Require Import UniMath.OrderTheory.OrderedSets.OrderedSets.