Definition append_vec : Vector X (S n). Proof. intros i. induction (natlehchoice4 (pr1 i) n (pr2 i)) as [c|d]. - exact (vec (pr1 i,,c)). - exact x. Defined.
Require Import UniMath.Combinatorics.Vectors. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Tactics.