Ssreflect Users Discussion List

[Frédéric Chyzak <>]

Benjamin, Georges, thanks for your comments.

 

On Wednesday 23 October 2013 09:54:48 Benjamin Werner wrote:

> Not about the error message but :

>

> Proving that equality proofs are equal cannot be done in general in Coq's

> type theory. (whether this is good, is bad, is a minor defect of the type

> theory, etc is another story). Here your lemma is true because equality is

> decidable over the considered type (boolean).

 

I had heard about these general facts.

 

> In SSR, this is proved generally for eqtypes by the lemma eq_irrelevance.

 

Probably I should have mentioned how I got the error message: I was doing the exercise of getting a proof of proof irrelevance for bool, just using Coq terms and ssreflect tactics. I am still trying to understand the fundamentals and at this point I am not aiming at a general decidable type, just at bool. So, I don't use eqtypes. Also, I am looking for a proof that speaks to me (== that I can explain to someone).

 

(Maybe I can make sense of the / switch after I got the fundamentals.)

 

Frédéric