proposition: Lemma WOlt_istrans (X : WellOrderedSet) : istrans (@WOlt X).
proof: Proof. intros x y z H1 H2 H3; simpl in *. apply (@squash_to_hProp _ (_,,isapropempty) (WO_istotal X y z)); intros [H|H]; simpl. - now apply H1, (WO_istrans X y z x H H3). - now apply H2. Qed.
imports: UniMath.MoreFoundations.DecidablePropositions UniMath.MoreFoundations.Propositions UniMath.MoreFoundations.Subtypes UniMath.MoreFoundations.Sets UniMath.MoreFoundations.AxiomOfChoice UniMath.Combinatorics.OrderedSets