Lemma map_concatenate {X Y} (f : X → Y) (r s : list X) : map f (r ++ s) = map f r ++ map f s. Proof. revert r. apply list_ind. - apply idpath. - intros x xs p. now rewrite mapStep, !concatenateStep, mapStep, p. Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Combinatorics.Vectors.