Definition concatenate_length {X} (x y:Sequence X) : length (concatenate x y) = length x + length y. Proof. intros. reflexivity. Defined.
Require Import UniMath.Combinatorics.Vectors. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Tactics.