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