fact: Definition transport_stn m n i (b:i<m) (p:m=n) : transportf stn p (i,,b) = (i,,transportf (λ m,i<m) p b).
imports: UniMath.Combinatorics.FiniteSets UniMath.Combinatorics.Lists UniMath.Combinatorics.Vectors UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Tactics