`X_CHOOSE_THEN : term -> thm_tactical`

SYNOPSIS
Replaces existentially quantified variable with given witness, and passes it to a theorem-tactic.

DESCRIPTION
X_CHOOSE_THEN expects a variable y, a tactic-generating function ttac, and a theorem of the form (A1 |- ?x. w) as arguments. A new theorem is created by introducing the given variable y as a witness for the object x whose existence is asserted in the original theorem, (w[y/x] |- w[y/x]). If the tactic-generating function ttac applied to this theorem produces results as follows when applied to a goal (A ?- t):
```    A ?- t
=========  ttac ({w[y/x]} |- w[y/x])
A ?- t1
```
then applying (X_CHOOSE_THEN `y` ttac (A1 |- ?x. w)) to the goal (A ?- t) produces the subgoal:
```    A ?- t
=========  X_CHOOSE_THEN `y` ttac (A1 |- ?x. w)
A ?- t1         (`y` not free anywhere)
```

FAILURE CONDITIONS
Fails if the theorem's conclusion is not existentially quantified, or if the first argument is not a variable. Failures may arise in the tactic-generating function. An invalid tactic is produced if the introduced variable is free in w or t, or if the theorem has any hypothesis which is not alpha-convertible to an assumption of the goal.

EXAMPLE
Suppose we have the following goal:
```  # g `!m n. m < n ==> m EXP 2 + 2 * m <= n EXP 2`;;
```
and rewrite with a theorem to get an existential antecedent:
```  # e(REPEAT GEN_TAC THEN REWRITE_TAC[LT_EXISTS]);;
val it : goalstack = 1 subgoal (1 total)

`(?d. n = m + SUC d) ==> m EXP 2 + 2 * m <= n EXP 2`
```
we may then use X_CHOOSE_THEN to introduce the name e for the existential variable and immediately substitute it in the goal:
```  # e(DISCH_THEN(X_CHOOSE_THEN `e:num` SUBST1_TAC));;
val it : goalstack = 1 subgoal (1 total)

`m EXP 2 + 2 * m <= (m + SUC e) EXP 2`
```
at which point ARITH_TAC will finish it.