The Coq mailing list

[Jesper Louis Andersen <jesper.louis.andersen AT gmail.com>]

The easiest way to "get at" information such as this is to use the built-in commands, Locate, Search and Check. Study them since they will save you a lot of hard work later on. In this case, typing

Locate "exists2".

will describe what the notation means. It is defined in http://coq.inria.fr/V8.4/stdlib/Coq.Init.Logic.html and it should also hint you toward your second question.

On Tue, Jan 1, 2013 at 7:04 PM, Victor Porton <porton AT narod.ru> wrote:

Please explain what is:

exists2 x:A, P & Q

Is it equivalent to

exists x:A, (P /\ Q)

?

--
Victor Porton - http://portonvictor.org

--
J.