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