`SUBST_ALL_TAC : thm -> tactic`

SYNOPSIS
Substitutes using a single equation in both the assumptions and conclusion of a goal.

DESCRIPTION
SUBST_ALL_TAC breaches the style of natural deduction, where the assumptions are kept fixed. Given a theorem A |- u = v and a goal ([A1;...;An] ?- t), SUBST_ALL_TAC (A |- u = v) transforms the assumptions A1,...,An and the term t into A1[v/u],...,An[v/u] and t[v/u] respectively, by substituting v for each free occurrence of u in both the assumptions and the conclusion of the goal.
```           {A1,...,An} ?- t
=================================  SUBST_ALL_TAC (A |- u = v)
{A1[v/u],...,An[v/u]} ?- t[v/u]
```
The assumptions of the theorem used to substitute with are not added to the assumptions of the goal, but they are recorded in the proof. If A is not a subset of the assumptions of the goal (up to alpha-conversion), then SUBST_ALL_TAC (A |- u = v) results in an invalid tactic. SUBST_ALL_TAC automatically renames bound variables to prevent free variables in v becoming bound after substitution.

FAILURE CONDITIONS
SUBST_ALL_TAC th (A ?- t) fails if the conclusion of th is not an equation. No change is made to the goal if no occurrence of the left-hand side of th appears free in (A ?- t).

EXAMPLE
```  # g `!p x y. 1 = x /\ p(x - 1) ==> p(x EXP 2 - x)`;;
```
and, as often, begin by breaking it down routinely:
```  # e(REPEAT STRIP_TAC);;
val it : goalstack = 1 subgoal (1 total)

0 [`1 = x`]
1 [`p (x - 1)`]

`p (x EXP 2 - x)`
```
Now we can use SUBST_ALL_TAC to substitute 1 for x in both assumptions and conclusion:
```  # e(FIRST_X_ASSUM(SUBST_ALL_TAC o SYM));;
val it : goalstack = 1 subgoal (1 total)

0 [`p (1 - 1)`]

`p (1 EXP 2 - 1)`
```
One can finish things off in various ways, e.g.
```  # e(POP_ASSUM MP_TAC THEN CONV_TAC NUM_REDUCE_CONV THEN REWRITE_TAC[]);;
```