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