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 CONDITIONS
Fails unless the conclusion of the theorem is unique-existentially quantified.
EXAMPLE
# let th = MESON[] `?!n. n = m`;;
...
val th : thm = |- ?!n. n = m
# EXISTENCE th;;
val it : thm = |- ?n. n = m