----------------------------------------------------------------------
EXISTS_LEFT1                                                   (Drule)
----------------------------------------------------------------------
EXISTS_LEFT1 : term -> thm -> thm

SYNOPSIS
Existentially quantifes hypotheses of a theorem.

KEYWORDS
existential, assumption, hypothesis

DESCRIBE
In this example, assume that {h1} and {h3} (only) involve the free variable {x}.

      h1, h2, h3 |- t
   --------------------- EXISTS_LEFT1 ``x``
   ?x. h1 /\ h3, h2 |- t


FAILURE
{EXISTS_LEFT1} will fail unless the term supplied is a free variable
which appears in one or more hypotheses but not the conclusion of the given
theorem

EXAMPLE
Where {th} is {[p, q, g x, h y, f x y] |- r}, and {fvx} and {fvy} are
{``x``} and {``y``},

{EXISTS_LEFT1 fvx th} is {[p, q, h y, ?x. g x /\ f x y] |- r}

{EXISTS_LEFT1 fvy th} is {[p, q, g x, ?y. h y /\ f x y] |- r}

COMMENTS
{EXISTS_LEFT1 fv} is just like {EXISTS_LEFT [fv]} except that
{EXISTS_LEFT1 fv} fails where {EXISTS_LEFT [fv]} returns the theorem unchanged

See {EXISTS_LEFT} for further discussion



SEEALSO
Drule.EXISTS_LEFT, Thm.CHOOSE, Thm.EXISTS, Tactic.CHOOSE_TAC,
Tactic.EXISTS_TAC.

----------------------------------------------------------------------