Definition drop_and_append' {X n} (x : stn (S n) -> X) : append (drop (S n,,x) (negpathssx0 _)) (x lastelement) = (S n,, x). Proof. intros. simpl. apply pair_path_in2. apply drop_and_append_vec. Defined.
Require Import UniMath.Combinatorics.Vectors. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Tactics.