Lemma foldr_concatenate {X Y : UU} (f : X → Y) (l : list X) : foldr concatenate [] (map (λ x, f x::[]) l) = map f l. Proof. revert l. apply list_ind. - apply idpath. - intros x l IH. now rewrite !map_cons, foldr_cons, IH. Qed.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Combinatorics.Vectors.