When applied to a theorem with a unique-existentially quantified
conclusion, EXISTENCE returns the same theorem with normal existential
quantification over the same variable.
A |- ?!x. p
------------- EXISTENCE
A |- ?x. p
FAILURE
Fails unless the conclusion of the theorem is unique-existentially quantified.