Introduces existential quantification using as witness a given free variable.
DESCRIPTION
When applied to a free variable term and a theorem,
SIMPLE_EXISTS gives the theorem made by existentially quantifying the
conclusion of the given theorem over the given free variable.
A |- p
------------- SIMPLE_EXISTS ``x``
A |- ?x. p
FAILURE
Fails if the term argument is not a free variable.
COMMENTS
The free variable need not appear in the conclusion of the theorem,
and may appear in the hypotheses.
EXAMPLE
- SIMPLE_EXISTS (Term `x`) (REFL (Term `x`));
> val it = |- ?x. x = x : thm
- SIMPLE_EXISTS (Term `x`) (REFL T);
> val it = |- ?x. T = T : thm