Definition transport_stn m n i (b:i<m) (p:m=n) : transportf stn p (i,,b) = (i,,transportf (λ m,i<m) p b). Proof. intros. induction p. reflexivity. Defined.
Require Import UniMath.Combinatorics.Vectors. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Tactics.