Definition composeSequence' {X m n} (f:stn n -> X) (g:stn m -> stn n) : Sequence X := functionToSequence (f ∘ g).
Require Import UniMath.Combinatorics.Vectors. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Tactics.