Definition flattenStep {X} (x: NonemptySequence (Sequence X)) : flatten x = concatenate (flatten (composeSequence' x (dni lastelement))) (lastValue x). Proof. intros. apply pair_path_in2. set (xlens := λ i, length(x i)). set (xvals := λ i, λ j:stn (xlens i), x i j). exact (flattenStep' xlens xvals). Defined.
Require Import UniMath.Combinatorics.Vectors. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Tactics.