The Coq mailing list

[robert dockins <robdockins AT fastmail.fm>]

This lemma is a consequence of dependent equality.  In module Eqdep from 
the standard library, the following lemma is proven:

Lemma UIP : forall (U:Type) (x y:U) (p1 p2:x = y), p1 = p2.



Haixing Hu wrote:
> This is an interesting problem. There is another simplified version: how to
> proof the floowing lemma?
>
> Lemma single_eq_proof : forall (A : Type) (x : A) (p1 p2 : x = x), p1 = p2.

> Quoting 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)?