Definition tallyStandardSubsetSegment {n : nat} (P : DecidableSubtype (⟦ n ⟧)) (i : ⟦ n ⟧) : ⟦ n ⟧. Proof. assert (k := tallyStandardSubset (λ j : ⟦ i ⟧, P (stnmtostnn i n (natlthtoleh i n (pr2 i)) j))). apply (stnmtostnn (S i) n). { apply natlthtolehsn. exact(pr2 i). } exact k. Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions. Require Import UniMath.MoreFoundations.Subtypes.