The Coq mailing list

[Nadeem Abdul Hamid <nadeem AT acm.org>]

I'm working on something where I try to prove properties of functions  
on some parameterized sets -- i.e.

Module Type SIG.

Parameter A : Set.
Parameter B : Set.

Parameter a_eq_dec : forall (a a':A), a = a' \/ a <> a'.

Parameter f : A -> B.
.... properties of f ...
End SIG.

(* followed by some proofs in another functor of SIG that uses  
properties of f *)


Now, I want to instantiate SIG with an implementation of A and B being  
a finite subset of natural numbers, e.g.

Definition A := { n:nat | n < 10 }.
Definition B := { n:nat | n < 10 }.

Lemma a_eq_dec : forall (a a':A), a=a' \/ a<>a'.
...

The problem here is that I can only seem to establish this by  
introducing the proof_irrelevance axiom.

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?

Thanks in advance,
nadeem