coq-club AT inria.fr

Subject: The Coq mailing list

List archive

chronological Thread

From: "Ethan Aubin" <ethan.aubin AT gmail.com>
To: coq-club AT pauillac.inria.fr
Subject: [Coq-Club] symmetric equality
Date: Sat, 29 Sep 2007 00:26:06 -0400
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=beta; h=received:message-id:date:from:to:subject:mime-version:content-type; b=gnwCLdy8CqlmwkYD1YXlbAO6tVzi/hbYw2boBqYNXrIXfuzuNlSbFr8GaaMF8CFk/r5P6rnOoKaeZusMfOdSgGbFezjFD/EVEoed94z2WyUxnnRZryOHcMouTKeXoRftYwgNUsbNVQ4y82t9WkX6S8D0uWaGhtx5Z6FMD2OrOPk=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Hi, This might be an obvious question, but is 'forall (A:Set)(x y:A), (x=y)=(y=x)' provable in Coq? - EA

[Coq-Club] symmetric equality, Ethan Aubin
- Re: [Coq-Club] symmetric equality, Stefan O'Rear
  - Re: [Coq-Club] symmetric equality, vsiles
  - Re: [Coq-Club] symmetric equality, Sean Wilson
    - Re: [Coq-Club] symmetric equality, Stefan O'Rear