The Coq mailing list

[Jean-Christophe Filliatre <filliatr AT lri.fr>]

You cannot prove an informative goal (in the sort Set) using a logical
hypothesis  (in the  sort Prop).  (Since logical  parts of  proofs are
removed during  extraction, it  would not be  possible to  extract the
computational contents of such a proof, where an informative object is
built from a logical one).

But you can prove

    { y:T | (P y) } -> T

or
        
    { y:T | (P y) } -> (EX y:T | (P y))

Best regards,
--Jean-Christophe.    

In his message of Wed August 18, 1999, Ewen Denney writes: 
> This must be easy, but I can't see what to do since Elim on the Intro's
> existential won't work.
> 
> How can I prove
> 
> (EX y:T | (P y))->T
> 
> or, indeed
> 
> (EX y:T | (P y))->{y:T | (P y)}
> 
> 
> Ewen

-- 
Jean-Christophe FILLIATRE
  
mailto:Jean-Christophe.Filliatre AT lri.fr
  http://www.lri.fr/~filliatr