SIMPLE_EXISTS : term -> thm -> thm
STRUCTURE
SYNOPSIS
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

SEEALSO
HOL  Kananaskis-13