Definition append_vec_compute_2 : append_vec lastelement = x. Proof. intros; unfold append_vec; simpl. induction (natlehchoice4 n n (natgthsnn n)) as [a|a]; simpl. - contradicts a (isirreflnatlth n). - reflexivity. Defined.
Require Import UniMath.Combinatorics.Vectors. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Tactics.