Lemma appendStep {X} (x y : X) (l : list X) : append x (y::l) = y::append x l. Proof. apply idpath. Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Combinatorics.Vectors.