----------------------------------------------------------------------
EXISTS_INTRO_IMP                                          (ConseqConv)
----------------------------------------------------------------------
EXISTS_INTRO_IMP : term -> thm -> thm

SYNOPSIS
Existentially quantifies both sides of an implication in the conclusion of a theorem.

KEYWORDS
rule, quantifier, universal.

DESCRIBE
When applied to a term {x} and a theorem {A |- t1 ==> t2}, the inference rule
{EXISTS_INTRO_IMP} returns the theorem {A |- (?x. t1) ==> (?x. t2)}, provided {x} is a
variable not free in any of the assumptions. There is no compulsion that {x}
should be free in {t1} or {t2}.

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




FAILURE
Fails if {x} is not a variable, the conclusion of the theorem is not an implication,
or if {x} is free in any of the assumptions.

EXAMPLE

   - val thm0 = mk_thm ([], Term `P (x:'a) ==> Q x`);
   > val thm0 =  |- P (x :'a) ==> Q x : thm

   - val thm1 = EXISTS_INTRO_IMP (Term `x:'a`) thm0;
   > val thm1 =  |- (?x. P x) ==> (?x. Q x)




SEEALSO
Thm.GEN, ConseqConv.GEN_IMP.

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