Definition partition {X n} (f:stn n -> nat) (x:stn (stnsum f) -> X) : Sequence (Sequence X). Proof. intros. exists n. exact (partition' f x). Defined.
Require Import UniMath.Combinatorics.Vectors. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Tactics.