Introduces an existential quantifier over a variable in a theorem.
DESCRIPTION
When applied to a pair consisting of a variable v and a theorem |- p,
SIMPLE_EXISTS returns the theorem |- ?v. p. It is not compulsory for v to
appear free in p, but otherwise the quantification is vacuous.
FAILURE CONDITIONS
Fails only if v is not a variable.
EXAMPLE
# SIMPLE_EXISTS `x:num` (REFL `x:num`);;
val it : thm = |- ?x. x = x
COMMENTS
The EXISTS function is more general: it can introduce an existentially
quantified variable to replace chosen instances of any term in the theorem.
However, SIMPLE_EXISTS is easier to use when the simple case is needed.