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