Lemma drop_full {A: UU} (l: list A): drop l (length l) = []. Proof. revert l; apply list_ind ; trivial. Defined.
Require Import UniMath.Foundations.NaturalNumbers. Require Import UniMath.Combinatorics.Vectors.