The Coq mailing list

[Andrej Bauer <andrej.bauer AT andrej.com>]

Since you're going down the setoids road, let me just preempt a
possible problem.

You originally wrote

>The construction in Blass's paper starts with a set Y = {u,v} of
>cardinality 2.  For every proposition P, he defines an equivalence
>relation R(P) on Y as follows:
>
> 1. (u,u) \in R(P)
> 2. (v,v) \in R(P)
> 3. P -> (u,v) \in R(P)
> 4. P -> (v,u) \in R(P).

This, strictly speaking, is not a definition. You might get one if you
required R(P) to be the least equivalence relation satisfying the
above 4 conditions.

But it is much easier to define R(P) as

R(P) = { (x,y) : Y x Y | x = y \/ P }.

No need for any inductive stuff. Also, Y is just bool.

In any case, it is probably useful to learn about setoids, but your
proof will be, at the end of the day, essentially a proof of decequiv
-> lem, but packaed up in the setoid technology.

With kind regards,

Andrej