Definition flatten_partition {X n} (f:stn n -> nat) (x:stn (stnsum f) -> X) : flatten (partition f x) ~ x. Proof. intros. intro i. change (x (weqstnsum1 f (pr1 (invmap (weqstnsum1 f) i),, pr2 (invmap (weqstnsum1 f) i))) = x i). apply maponpaths. apply subtypePath_prop. now rewrite homotweqinvweq. Defined.
Require Import UniMath.Combinatorics.Vectors. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Tactics.