`SUBGOAL_THEN : term -> thm_tactic -> tactic`
STRUCTURE
SYNOPSIS
Allows the user to introduce a lemma.
DESCRIPTION
The user proposes a lemma and is then invited to prove it under the current assumptions. The lemma is then used with the thm_tactic to simplify the goal. That is, if
```    A1 ?- t1
==========  f (u |- u)
A2 ?- t2
```
then
```         A1 ?- t1
====================  SUBGOAL_THEN u f
A1 ?- u   A2 ?- t2
```

Typically f (u |- u) will be an invalid tactic because it would return a validation function which generated the theorem A1,u |- t1 from the theorem A2 |- t2. Nonetheless, the tactic SUBGOAL_THEN u f is valid because of the extra sub-goal where u must be proved.

FAILURE
SUBGOAL_THEN will fail if an attempt is made to use a nonboolean term as a lemma.
USES
When combined with rotate, SUBGOAL_THEN allows the user to defer some part of a proof and to continue with another part. SUBGOAL_THEN is most convenient when the tactic solves the original goal, leaving only the subgoal. For example, suppose the user wishes to prove the goal
```   {n = SUC m} ?- (0 = n) ==> t
```
Using SUBGOAL_THEN to focus on the case in which ~(n = 0), rewriting establishes it truth, leaving only the proof that ~(n = 0). That is,
```   SUBGOAL_THEN (Term `~(0 = n)`) (fn th => REWRITE_TAC [th])
```
generates the following subgoals:
```   {n = SUC m} ?-  ~(0 = n)
?- T
```