Lemma wosub_le_isrefl {X:hSet} : isrefl (wosub_le X). 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.
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.