The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

No.  For example, the type

Inductive bool_in_prop : Prop := trueP | falseP.

does not have provable irrelevance.  (You can neither proof [trueP = falseP] nor [trueP <> falseP].)  It is clearly decidable, though, because [left trueP : {bool_in_prop} + {~bool_in_prop}].

I'm not sure if there's a general way to make such proofs, but I suspect there might be, at least for inductively defined [Prop]s.

For your specific case, I think you might need to assume functional extensionality (and then prove trivially that all inhabitants of [False] are equal).  Otherwise, I think there is no way to prove a non-trivial function equality, though I may be wrong.

-Jason

On Tuesday, October 22, 2013, Ilmārs Cīrulis wrote:

Is it true that for all decidable Prop there is provable proof irrelevance?

If it's true, is there any general way how to make such proofs?

Also more specifically - how I can prove that
forall (n m:nat) (p1 p2: n<>m), p1 = p2 ?