The Coq mailing list

[Areski Nait Abdallah <areski AT pauillac.inria.fr>]

> (1) Any tactic works just as well for a goal of type Prop or of type Set

        >> exept eventually the elimination of the existential quantifier 
        >> (for technical reasons).

These exception and technical reasons is precisely what my question is about.

As an example : Assume
   1. I have a proof of A \/ B.
   2. I have a proof of A -> { x : E | P }
   3. I have a proof of B -> { x : E | P }
When and under which conditions do I combine these into a proof of 
   4. A \/ B -> { x : E | P } , 
and why are these conditions necessary ?


Thanks.
A.


> 
> Cody
> 
> On Wed, 2007-12-19 at 15:17 +0100, Areski Nait Abdallah wrote:
> > Hello,
> > 
> > I am looking for a reference which discusses 
> > 
> >     (1) which tactis can be used for solving a goal of type Set, and 
> > 
> >     (2) covers the rationale for such tactics.
> > 
> > Thank you for your help,
> > 
> > Areski
> >