Lemma upto'_eqn {X:hSet} (g : choice_fun X) (C D : WOSubset X) (j : C ≼ D) (c : C) (d : D) : pr1 (subtype_inc (pr1 j) c) = pr1 d -> pr1 (g (upto' c)) = pr1 (g (upto' d)). Proof. intros p. assert (e' : upto' c = upto' d). { apply subtypePath_prop. change (upto c = upto d). assert (q : subtype_inc (pr1 j) c = d). { now apply subtypePath_prop. } clear p. induction q. now apply upto_eqn. } now induction e'. 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.