PEXISTENCE
PairRules.PEXISTENCE : (thm -> thm)
Deduces paired existence from paired unique existence.
When applied to a theorem with a paired unique-existentially quantified
conclusion, EXISTENCE returns the same theorem with normal paired
existential quantification over the same pair.
A |- ?!p. t
------------- PEXISTENCE
A |- ?p. t
Failure
Fails unless the conclusion of the theorem is a paired unique-existential quantification.