Lemma vec_append_lid {A : UU} (u : vec A 0) {n} : vec_append u = idfun (vec A n). Proof. induction u. reflexivity. Defined.
Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Foundations.NaturalNumbers.