{A : Type} (n : nat) (l : list A) (H : (length l <= n)%nat) : remove n l = l. Proof. unfold remove. rewrite take_length_leq. 2: exact _. rewrite drop_length_leq. 2: exact _. apply app_nil. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc Require Import Types.Paths Types.Unit Types.Prod Types.Sigma Types.Sum