Definition drop' {X} (x:Sequence X) : x != nil -> Sequence X. Proof. intros h. exact (drop x (pr2 (logeqnegs (nil_length x)) h)). Defined.
Require Import UniMath.Combinatorics.Vectors. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Tactics.