----------------------------------------------------------------------
MK_PEXISTS                                                 (PairRules)
----------------------------------------------------------------------
MK_PEXISTS : (thm -> thm)

KEYWORDS
rule, quantifier, existential, equality.

LIBRARY
pair

SYNOPSIS
Existentially quantifies both sides of a universally quantified
equational theorem.

DESCRIBE
When applied to a theorem {A |- !p. t1 = t2}, the inference rule {MK_PEXISTS}
returns the theorem {A |- (?x. t1) = (?x. t2)}.

       A |- !p. t1 = t2
   --------------------------  MK_PEXISTS
    A |- (?p. t1) = (?p. t2)




FAILURE
Fails unless the theorem is a singly paired universally quantified equation.

SEEALSO
PairRules.PEXISTS_EQ, PairRules.PGEN, PairRules.LIST_MK_PEXISTS,
PairRules.MK_PABS.

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