The Coq mailing list

[ahrens <Benedikt.Ahrens AT unice.fr>]

Hi,

On 06/28/2011 03:25 PM, Gert Smolka wrote:
[...]
> 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.

you might be interested in the blog post [1], which explains the
theoretical issues and mentions precisely your example of finite sets.

Greetings,
benedikt

[1]
http://homotopytypetheory.org/2011/04/10/just-kidding-understanding-identity-elimination-in-homotopy-type-theory/