Definition WOlt' (X : WellOrderedSet) (x y : X) : hProp. Proof. exists ((x ≤ y) × (x != y))%type. abstract (now apply isapropdirprod; [ apply propproperty | apply isapropneg ]). Defined.
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.