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. intros. induction e. apply subtypePath_prop. apply idpath. Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.