Lemma reverse_reverse {X} (r : list X) : reverse (reverse r) = r. Proof. revert r. apply list_ind. - apply idpath. - intros x xs p. now rewrite !reverseStep, reverse_append, p. Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Combinatorics.Vectors.