proposition: Lemma foldr1_concatenate {X Y : UU} (f : X → Y) (l : list X) : map f l = foldr1 concatenate [] (map (λ x, f x::[]) l).
proof: Proof. revert l. apply list_ind. - apply idpath. - intros x. refine (list_ind _ _ _). + intro. apply idpath. + intros x' l _ IH. exact (maponpaths (cons (f x)) IH). Defined.
imports: UniMath.MoreFoundations.Tactics UniMath.Combinatorics.StandardFiniteSets UniMath.Combinatorics.Vectors