The Coq mailing list

[Eduardo Gimenez <Eduardo.Gimenez AT trusted-logic.fr>]

Hello,

I am afraid that this is simply not provable in Coq: is like saying that 
(A,B,C:Prop)(A/\B->C)==(B/\A->C). You should not confuse being logically 
equivalent (ie, the existence of a function transforming each proof of the 
right hand side proposition into a proof of the left hand side one) with 
being intentionally equal (ie, being exactly the same statement, up to the 
computation rules).

Best wishes,
Eduardo.


On Wednesday 27 August 2003 11:06, Jean-Yves Vion-Dury wrote:
> 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