Definition append_vec_compute_1 i : append_vec (dni lastelement i) = vec i. Proof. intros. induction i as [i b]; simpl. rewrite replace_dni_last. unfold append_vec; simpl. induction (natlehchoice4 i n (natlthtolths i n b)) as [p|p]. - simpl. apply maponpaths. apply isinjstntonat; simpl. reflexivity. - simpl. destruct p. induction (isirreflnatlth i b). Defined.
Require Import UniMath.Combinatorics.Vectors. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Tactics.