Lemma foldr1_map_concatenate {X Y : UU} (f : X → Y) (l : list X) : map f l = foldr1_map concatenate [] (λ x, f x::[]) l. Proof. set (P := fun xs res => map f xs = res). refine (foldr1_map_ind _ _ _ P _ _ _ l). - apply idpath. - intro; apply idpath. - intros x' l' x'' res Hyp. exact (maponpaths (cons (f x'')) Hyp). Qed.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Combinatorics.Vectors.