Definition flattenUnorderedSequence {X : UU} : UnorderedSequence (UnorderedSequence X) -> UnorderedSequence X. Proof. intros x. use tpair. - exact ((∑ i, pr1 (x i))%finset). - intros ij. exact (x (pr1 ij) (pr2 ij)). Defined.
Require Import UniMath.Combinatorics.Vectors. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Tactics.