Definition flatten {X : UU} : Sequence (Sequence X) -> Sequence X. Proof. intros x. exists (stnsum (length ∘ x)). exact (flatten' (sequenceToFunction ∘ x)). Defined.
Require Import UniMath.Combinatorics.Vectors. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Tactics.