The Coq mailing list

["Stefan O'Rear" <stefanor AT cox.net>]

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

Attachment: signature.asc
Description: Digital signature