Definition wosub_inc {X:hSet} {S T : WOSubset X} : (S ≼ T) -> S -> T. Proof. intros le s. exact (subtype_inc (pr1 le) s). 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.