proposition: Lemma drop_and_append_vec {X n} (x : Vector X (S n)) : append_vec (x ∘ dni_lastelement) (x lastelement) = x.
proof: 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.
imports: UniMath.Combinatorics.FiniteSets UniMath.Combinatorics.Lists UniMath.Combinatorics.Vectors UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Tactics