The Coq mailing list

[Li-Yang Tan <lytan AT artsci.wustl.edu>]

Hello,

I have a simple question regarding the intro(s) tactic.  Suppose I am
trying to prove the following implication,

P : Prop
Q : Prop
----------------------------------
(P /\ (Q /\ R)) -> ((P /\ Q) /\ R)

I can pull to antecedent of the implication into my list of
hypotheses/assumptions by doing "intros [H1 [H2 H3]]".  This is very
nice, since it saves me from having to do: "intro; elim H; intros; elim
H0; intros."  I believe there is a similar trick for disjunctions, so if
the antecedent of my implication is say (P /\ (Q \/ R)), I can simply do
"intros [H1 [H2 | H3]]."

I am curious as to whether there is something similar if the antecedent
has a list of nested existential quantifiers.

For example, consider the following:

Theorem Fermat :
   (exists x, exists y, exists z, exists n,
      (n > 2) /\ (x^n + y^n  = z^n)) -> False.

Is there any way I can introduce x, y, z, and n into my assumptions
*without* having to do the following?

intro.
elim H; intros.
elim H0; intros.
elim H1; intros.
elim H2; intros.

Thanks in advance,
Li-Yang Tan