Lemma concatenateStep {X} (x:X) (r s:list X) : (x::r) ++ s = x :: (r ++ s). Proof. apply idpath. Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Combinatorics.Vectors.