The Coq mailing list

[Jonas Oberhauser <s9joober AT gmail.com>]

Hi everyone,

I got a little confused by an error message in Coq 8.3. This is a broken 
down example that reproduces the message:

Inductive P : Prop := p : nat -> P.

Goal forall x y, p x = p y -> x = y.
intros x y. intros e. injection e.

"Error: Nothing to do, it is an equality between convertible terms."

I assume this is because we don't want to scare proof irrelevance away. 
It seems a little bit harsh, though, since I'm unable to prove eg "p 4 = 
p 2" without assuming PI. So I don't think p 4 and p 2 are convertible. 
(nor do I think p x and p y are, in general).

Kind regards, jonas