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

SYNOPSIS
Existentially quantifies both the antecedent and consequent of an implication.

KEYWORDS
rule, quantifier, existential, implication.

DESCRIBE
When applied to a variable {x} and a theorem {A |- t1 ==> t2}, the
inference rule {EXISTS_IMP} returns the theorem {A |- (?x. t1) ==> (?x. t2)},
provided {x} is not free in the assumptions.

         A |- t1 ==> t2
   --------------------------  EXISTS_IMP "x"   [where x is not free in A]
    A |- (?x.t1) ==> (?x.t2)




FAILURE
Fails if the theorem is not implicative, or if the term is not a variable, or
if the term is a variable but is free in the assumption list.

SEEALSO
Drule.EXISTS_EQ.

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