Lemma append_and_drop_fun {X n} (x : stn n -> X) y : append_vec x y ∘ dni lastelement = x. Proof. intros. apply funextsec; intros i. simpl. unfold append_vec. induction (natlehchoice4 (pr1 (dni lastelement i)) n (pr2 (dni lastelement i))) as [I|J]. - simpl. apply maponpaths. apply subtypePath_prop. simpl. apply di_eq1. exact (stnlt i). - apply fromempty. simpl in J. assert (P : di n i = i). { apply di_eq1. exact (stnlt i). } induction (!P); clear P. induction i as [i r]. simpl in J. induction J. exact (isirreflnatlth _ r). Defined.
Require Import UniMath.Combinatorics.Vectors. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Tactics.