Definition flatten {X} : list (list X) → list X. Proof. apply list_ind. + exact []. + intros s _ f. exact (concatenate s f). Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Combinatorics.Vectors.