Definition drop {A: UU} (l: list A) (n: nat): list A. Proof. revert l. induction n. - exact (idfun _). - apply list_ind. + exact []. + intros x xs _. exact (IHn xs). Defined.
Require Import UniMath.Foundations.NaturalNumbers. Require Import UniMath.Combinatorics.Vectors.