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