The Coq mailing list

[Edsko de Vries <devriese AT cs.tcd.ie>]

Hi,

Just to say: independently of whether using setoids helps me with the
problem I really need to solve, it has certainly made all my proofs in
BooleanAlgebraM much nicer :) Thanks! New formalization available at

http://www.cs.tcd.ie/~devriese/coq

(By the way, this does not yet include the proof that True is not
equivalent to False, because the proof as suggested on this list is a
semantic proof, and I had generalized the module so that I cannot write
the semantic interpretation function -- I might have to change that
again.)

Edsko