The Coq mailing list

[darktenaibre <darktenaibre AT isomorphis.me>]

Ah,  that notprop predicate prevents this stupid observation though. You 
can certainly write something like (fun T => forall P : Prop, ~ (@eq 
Type P T)) which will easily block the previous proof, but it's probably 
unusable this way. I do not have any idea for a clever solution to this 
problem though.
On 04/24/2016 02:32 AM, darktenaibre wrote:
> On 04/24/2016 02:21 AM, Jonathan Leivent wrote:
> > Definition proof_uninformativeness := forall (P : Prop)(S : Set)(f : 
> > P -> S)(p1 p2 : P), f p1 = f p2. 
> Hi,
> If you take f:=id, isn't it just proof irrelevance ?
>
>
> Lemma proof_uninformativeness_irrelevance : proof_uninformativeness -> 
> forall (P : Prop) (p q : P), p = q.
>   intros pu P; apply pu.
> Qed.