The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Hi Patricia, 

  I guess you wanted to send this to coq-club AT inria.fr instead of coqdev AT inria.fr which is the developer mailing list.

The short answer is you cannot eliminate an existential in Prop to 

something in Set. This is a difference with the subset type {x : A | P x} which is also available in Coq.

Best,

-- Matthieu

On Wed, Nov 18, 2015 at 4:32 PM Patricia Peratto <psperatto AT vera.com.uy> wrote:

I'm making a proof that involves the existential quantifier.

I'want to get from a proof of a formula with this

quantifier the element that exists and the proof

of the proposition, i.e. "a" in the theorem below.

Theorem elem (A:Set)(P:A->Prop) :
(exists a:A, P a) -> A.
intro.
elim H.

When I try to prove elem, in elim H, I get

the message:

Error: Cannot find the elimination combinator ex_rec, the elimination of the
inductive definition ex on sort Set is probably not allowed.

How can I do to get "a" and the proof of "(P a)"?

Regards

Patricia