`CHOOSE_TAC : thm_tactic`

SYNOPSIS
Adds the body of an existentially quantified theorem to the assumptions of a goal.

DESCRIPTION
When applied to a theorem A' |- ?x. t and a goal, CHOOSE_TAC adds t[x'/x] to the assumptions of the goal, where x' is a variant of x which is not free in the assumption list; normally x' is just x.
```         A ?- u
====================  CHOOSE_TAC (A' |- ?x. t)
A u {t[x'/x]} ?- u
```
Unless A' is a subset of A, this is not a valid tactic.

FAILURE CONDITIONS
Fails unless the given theorem is existentially quantified.

EXAMPLE
Suppose we have a goal asserting that the output of an electrical circuit (represented as a boolean-valued function) will become high at some time:
```   ?- ?t. output(t)
```
and we have the following theorems available:
```   t1 = |- ?t. input(t)
t2 = !t. input(t) ==> output(t+1)
```
Then the goal can be solved by the application of:
```   CHOOSE_TAC t1 THEN EXISTS_TAC `t+1` THEN
UNDISCH_TAC `input (t:num) :bool` THEN MATCH_ACCEPT_TAC t2
```