The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Nadeem Abdul Hamid wrote:
> Definition A := { n:nat | n < 10 }.
>
> ...
>
> So the question is: Does anyone have other suggestions for defining 
> concrete instantiations of A and B as finite subsets of the natural 
> numbers, that would allow proof of the a_eq_dec property without 
> introducing proof irrelevance?

This is the standard definition that I use:

Inductive fin : nat -> Type :=
  | FO : forall n, fin (S n)
  | FS : forall n, fin n -> fin (S n).