proposition: Lemma iswofun_idfun {X : WellOrderedSet} : iswofun (idfun X).
proof: Proof. split. - now intros x. - intros x y hxy. now apply hinhpr; exists y. Qed.
imports: UniMath.MoreFoundations.DecidablePropositions UniMath.MoreFoundations.Propositions UniMath.MoreFoundations.Subtypes UniMath.MoreFoundations.Sets UniMath.MoreFoundations.AxiomOfChoice UniMath.Combinatorics.OrderedSets