Lemma drop_and_append_vec {X n} (x : Vector X (S n)) : append_vec (x ∘ dni_lastelement) (x lastelement) = x. Proof. intros. apply funextfun; intros [i b]. simpl. induction (natlehchoice4 i n b) as [p|p]. - simpl. unfold append_vec. simpl. induction (natlehchoice4 i n b) as [q|q]. + simpl. apply maponpaths. apply isinjstntonat; simpl. reflexivity. + induction q. contradicts p (isirreflnatlth i). - induction p. unfold append_vec; simpl. induction (natlehchoice4 i i b) as [r|r]. * simpl. apply maponpaths. apply isinjstntonat; simpl. reflexivity. * simpl. apply maponpaths. apply isinjstntonat; simpl. reflexivity. Defined.
Require Import UniMath.Combinatorics.Vectors. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Tactics.