Lemma foldr1_concatenate {X Y : UU} (f : X → Y) (l : list X) : map f l = foldr1 concatenate [] (map (λ x, f x::[]) l). Proof. simple refine (foldr1_map_concatenate _ _ @ _). apply foldr1_foldr1_map. Qed.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Combinatorics.Vectors.