{A : Type} (n : nat) (l : list A) : list A := match l, n with | _ :: l, n.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc Require Import Types.Paths Types.Unit Types.Prod Types.Sigma Types.Sum