proposition: 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: 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.
imports: UniMath.MoreFoundations.DecidablePropositions UniMath.MoreFoundations.Propositions UniMath.MoreFoundations.Subtypes UniMath.MoreFoundations.Sets UniMath.MoreFoundations.AxiomOfChoice UniMath.Combinatorics.OrderedSets