Lemma drop_step {A: UU} (x: A) (xs: list A) (n: nat) : drop (x :: xs) (S n) = drop xs n. Proof. apply idpath. Defined.
Require Import UniMath.Foundations.NaturalNumbers. Require Import UniMath.Combinatorics.Vectors.