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