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