The Coq mailing list

[Gert Smolka <smolka AT ps.uni-saarland.de>]

There are many ways to define a function
Fin : nat -> Type such that the type Fin n
has n elements.  I tried the following:

Inductive Fin : nat -> Type :=
| FinO : forall n, Fin (S n)
| FinS : forall n, Fin n -> Fin (S n).

Unfortunately, I cannot prove

Lemma Fin1 (k : Fin 1) :
k = FinO 0.

Help would be appreciated.
Also, what is the "standard" way to define Fin?

Gert