The Coq mailing list

[vsiles AT lix.polytechnique.fr]

> On Sat, Sep 29, 2007 at 12:26:06AM -0400, Ethan Aubin wrote:
>> Hi,  This might be an obvious question, but is 'forall (A:Set)(x y:A),
>> (x=y)=(y=x)' provable in Coq? - EA
>
> Equality is a very slippery subject in Coq and other systems based on
> intuitionistic type theories.  Your statement is certainly true if you
> replace the outer = with <-> (split; auto).  In general, it's a bad idea
> to use = on anything other than values of inductive types.
>
> Stefan
>
You also need (maybe it's too strong) the equality on A to be decidable
(forall x y:A, {x=y}+{x<>y}), otherwise you're not always allowed to test
x against any y of A.

Vincent