coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] How to prove (a,b:Z) a=b == b=a ?

From: Jean-Yves Vion-Dury <jean-yves.vion-dury AT inrialpes.fr>
To: coq-club AT pauillac.inria.fr
Subject: [Coq-Club] How to prove (a,b:Z) a=b == b=a ?
Date: Wed, 27 Aug 2003 11:06:58 +0200
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Organization: Inria Rhones-Alpes

Probably this is simple for many of you.

Unfortunately, as a beginner, I can't find a simple elegant solution (nor the uggly one, I must say...).

I wanted to use sym_eq , but I can't find out how to apply it to a subterm of the goal...

Many thanks in advance.
Jean-Yves

Jean-Yves Vion-Dury Research Scientist	Xerox Research Centre Europe
INRIA (sabbatical) 655 avenue de l'Europe, 38334 Montbonnot (FRANCE) Jean-Yves.Vion-Dury AT inrialpes.fr	from France: 0 4 76 61 53 83 from abroad: +33 4 76 61 53 83
you may have a look at the Circus Transformation Language?	www.alphaAve.com

[Coq-Club] How to prove (a,b:Z) a=b == b=a ?, Jean-Yves Vion-Dury
- Re: [Coq-Club] How to prove (a,b:Z) a=b == b=a ?, Eduardo Gimenez