Lemma map_append {X Y} (f : X → Y) (x : X) (r : list X) : map f (append x r) = append (f x) (map f r). Proof. exact (map_concatenate _ _ _). Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Combinatorics.Vectors.