Definition drop {X} (x:Sequence X) : length x != 0 -> Sequence X. Proof. revert x. intros [n x] h. induction n as [|n]. - simpl in h. contradicts h (idpath 0). - exact (n,,x ∘ dni_lastelement). Defined.
Require Import UniMath.Combinatorics.Vectors. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Tactics.