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