Is there a way to prove the following theorem in Coq?
Theorem bool_pirrel : forall (b : bool) (p1 p2 : b = true), p1 = p2.
EDIT: An attempt to give a brief explanation for "what proof irrelevance is" (correct me someone if I am wrong or inaccurate)
The basic idea is that in the proposition world (or the
Prop sort in Coq), what you (and you should) really care about is the provability of a proposition, not the proofs of it, there may be many (or none). In case you have multiple proofs, from the provability point of view, they are equal in the sense that they prove the same proposition. So their distinction is just irrelevant. This differs from the computational point of view where you really care about the distinction of two terms, e.g., basically, you don't want the two inhabitants of the
bool type (or
Set in Coq's words), namely
false to be equal. But if you put them in
Prop, they are treated equal.