The Coq mailing list

[Satrajit Roy <satrajit.roy AT gmail.com>]

Also, I found an exercise in an older book (circa 1990s) which reads something like: prove that (A=>B)=>(B=>A)

I wrote :

Theorem foo: forall a b:Prop, (a->b)->(b->a).
But I cannot prove  foo.

Of course if I write:

Theorem foo':forall a b:Prop, a->(a->b)->(b->a) , it seems logical to assume a and is provable as well.
But it doesn't seem like foo and foo' equivalent, are they?

On Wed, Feb 9, 2011 at 5:51 PM, Satrajit Roy <satrajit.roy AT gmail.com> wrote:

What is the correct way to express statements like the following in the Coq environment?

for all x, exists y such that A(x, y) =>  exists y, for all x such that A(x, y) and the converse of it
--

Satrajit

-- 

Satrajit