proposition: Lemma transport_stn {m n : nat} (e: m=n) (i: ⟦m⟧ ) : transportf stn e i = make_stn n (pr1 i) (transportf (λ k, pr1 i < k) e (pr2 i)).
proof: Proof. intros. induction e. apply subtypePath_prop. apply idpath. Defined.
imports: UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions UniMath.MoreFoundations.NegativePropositions