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