Definition concatenate_0 {X} (s t:Sequence X) : length t = 0 -> concatenate s t = s. Proof. induction s as [m s]. induction t as [n t]. intro e; simpl in e. induction (!e). simple refine (sequenceEquality2 _ _ _ _). - simpl. apply natplusr0. - intro i; simpl in i. simpl. unfold concatenate'. rewrite weqfromcoprodofstn_invmap_r0. simpl. reflexivity. Defined.
Require Import UniMath.Combinatorics.Vectors. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Tactics.