MK_PEXISTS
PairRules.MK_PEXISTS : (thm -> thm)
Existentially quantifies both sides of a universally quantified equational theorem.
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.
See also
PairRules.PEXISTS_EQ,
PairRules.PGEN,
PairRules.LIST_MK_PEXISTS,
PairRules.MK_PABS