length_drop@{i|} {A : Type@{i}} (n : nat) (l : list A) : length (drop n l) = (length l - n)%nat. Proof. induction l as [|a l IHl] in n |- * using list_ind@{i i}. 1: by rewrite drop_nil. destruct n. 1: reflexivity. exact (IHl n). Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc Require Import Types.Paths Types.Unit Types.Prod Types.Sigma Types.Sum