proposition: Lemma assoc_concatenate {X} (r s t : list X) : (r ++ s) ++ t = r ++ (s ++ t).
proof: Proof. revert r. apply list_ind. - apply idpath. - intros x xs p. now rewrite !concatenateStep, p. Defined.
imports: UniMath.MoreFoundations.Tactics UniMath.Combinatorics.StandardFiniteSets UniMath.Combinatorics.Vectors