Introduces a paired existential quantification in place of a paired choice.
DESCRIPTION
The inference rule PEXISTS_RULE expects a theorem asserting that
(@p. t) denotes a pair for which t holds.
The equivalent assertion that there exists a p for which t holds is
returned.
A |- t[(@p. t)/p]
------------------ PEXISTS_RULE
A |- ?p. t
FAILURE
Fails if applied to a theorem the conclusion of which is not
of the form (t[(@p.t)/p]).