{A : Type} (l : list A) (H : length l = 0%nat) : l = nil. Proof. destruct l. - reflexivity. - discriminate. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc Require Import Types.Paths Types.Unit Types.Prod Types.Sigma Types.Sum