The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Gert Smolka wrote:
> 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?

Have you read the chapter "Dependent Data Structures" from CPDT?
    http://adam.chlipala.net/cpdt/
I think there's a fair chance it would answer not only these questions, 
but also others likely to be encountered when working with such datatypes.