Section vacio.
Require Export List.
Variable A:Set.
Inductive empty :list A -> Prop :=
   nul:(empty nil).

Check empty_ind.

Lemma nempty:forall (a:A) (l: list A), ~(empty (a::l)).
intros.
intro ne.
inversion  ne.
Qed.
End vacio.

Check empty.
Check nempty.

