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