Lemma append_concatenate {X} (x : X) (l s : list X) : append x (l ++ s) = l ++ append x s. Proof. apply assoc_concatenate. Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Combinatorics.Vectors.