proposition: Lemma wosub_le_isrefl {X:hSet} : isrefl (wosub_le X).
proof: Proof. intros S. use tpair. + intros x xinS. exact xinS. + split. * intros s s' le. exact le. * intros s s' Ss Ss' le. exact Ss'. Defined.
imports: UniMath.MoreFoundations.DecidablePropositions UniMath.MoreFoundations.Propositions UniMath.MoreFoundations.Subtypes UniMath.MoreFoundations.Sets UniMath.MoreFoundations.AxiomOfChoice UniMath.Combinatorics.OrderedSets