Definition stn_predicate {n : nat} (P : ⟦n⟧ -> UU) (k : nat) (h h' : k < n) : P (k,,h) -> P (k,,h'). Proof. intros H. transparent assert (X : (h = h')). - apply propproperty. - exact (transportf (λ x, P (k,,x)) X H). Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.