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