The Coq mailing list

[Cedric.Auger AT lri.fr]

I want to make very simple enumerated types,
so I did:

Inductive enums : nat -> Set :=
| New : forall n, enums n
| Old : forall n, enums n -> enums (S n).
Implicit Arguments New [n].
Implicit Arguments Old [n].

Set Printing All.

Lemma e : forall (e : enums 0), e = New.
intros.
(*
Now I want to destruct e
*)
induction e.
(*
all occurences of O have been replaced by n,
so it "generalize" instead of instantiate,
and our proof cannot succeed this way
*)

is there anyway to prove this lemma, or to implement
enumerated types without using Fsets & co, and without using
like enums m = {n | m < n}?