coq-club AT inria.fr

Subject: The Coq mailing list

List archive

witness of existential

From: Ewen Denney <denney AT irisa.fr>
To: coq AT pauillac.inria.fr
Subject: witness of existential
Date: Wed, 18 Aug 1999 12:57:27 +0200
Organization: IRISA, Campus de Beaulieu, 35042 Rennes Cedex, France

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

witness of existential, Ewen Denney
- Re: witness of existential, Jean-Christophe Filliatre
- Re: witness of existential, Benjamin Werner
  - Re: witness of existential, Ewen Denney
    - Re: witness of existential, Benjamin Werner