Proof irrelevance

On 6/11/14 8:15 AM, Jason Gross wrote:
>
> In theories/Init/Logic.v:
>
> > @@ -609,3 +609,12 @@ Qed.
> >
> >  Declare Left Step iff_stepl.
> >  Declare Right Step iff_trans.
> > +
> > +Section conj_proof_irrelevance.
> > +  Local Notation "'pip' P"  := (forall (p1 p2 : P), p1 = p2)(at level 80).
>
> Note: You can do |Local Notation pip P := (forall p1 p2 : P, p1 = 
> p2).|, and then you don't need |at level 80|, and don't make |pip| 
> into a symbol. (Also, I'm curious, why |pip|, rather than |uip|?)
>
> —
> Reply to this email directly or view it on GitHub 
> <https://github.com/coq/coq/pull/44/files#r19929574>.
>
My guess is : pip for "proof irrelevance property"

"uip" is only for uniqueness of identity proofs,  this mean that P would 
have to be an equality proof.

Yves