The Coq mailing list

[robert dockins <robdockins AT fastmail.fm>]

I'm playing around with well-specified types and tried to prove 
something like the following :

Parameter limit:nat.
Definition nat_subset := { n:nat | n < limit }.
Lemma eq_nat_subset_dec : forall x y:nat_subset, {x=y}+{x<>y}.


I've had great difficulties, however.  The problem comes down to showing 
that two proofs of (x<limit) are equivalent.  From the definition of 
'le' it seems pretty clear that this is the case.  However I run into 
problems with second-order unification and the restrictions between the 
Prop and Set universes with all the techniques I have tried.  Is it 
possible to prove a goal like this one without resorting to classic (and 
hence proof irrelevance)?