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