{A : Type} (l : list A) : remove 0 l = tail l. Proof. unfold remove. by rewrite take_0, drop_1. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc Require Import Types.Paths Types.Unit Types.Prod Types.Sigma Types.Sum