Definition vec_append {A : UU} {m} (u : vec A m) {n} (v : vec A n) : vec A (m + n) := vec_ind (λ (p : nat) (_ : vec A p), vec A (p + n)) v (λ (x : A) (p : nat) (_ : vec A p) (w : vec A (p + n)), x ::: w) m u.
Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Foundations.NaturalNumbers.