Lemma reverse_concatenate {X} (l s : list X) : reverse (l ++ s) = reverse s ++ reverse l. Proof. revert l. apply list_ind. - symmetry. apply concatenate_nil. - intros x xs p. now rewrite concatenateStep, !reverseStep, p, append_concatenate. Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Combinatorics.Vectors.