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