Definition empty_woset : WellOrderedSet. Proof. exists (_,,isasetempty). use tpair. - intros []. - abstract (repeat split; try (now intros []); now intros T t'; apply (squash_to_hProp t'); intros [[]]). 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.