Definition append {X} : Sequence X -> X -> Sequence X. Proof. intros x y. exact (S (length x),, append_vec (pr2 x) y). Defined.
Require Import UniMath.Combinatorics.Vectors. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Tactics.