`SUBST1_TAC : thm_tactic`
STRUCTURE
SYNOPSIS
Makes a simple term substitution in a goal using a single equational theorem.
DESCRIPTION
Given a theorem A'|-u=v and a goal (A,t), the tactic SUBST1_TAC (A'|-u=v) rewrites the term t into t[v/u], by substituting v for each free occurrence of u in t:
```      A ?- t
=============  SUBST1_TAC (A'|-u=v)
A ?- t[v/u]
```
The assumptions of the theorem used to substitute with are not added to the assumptions of the goal but are recorded in the proof. If A' is not a subset of the assumptions A of the goal (up to alpha-conversion), then SUBST1_TAC (A'|-u=v) results in an invalid tactic.

SUBST1_TAC automatically renames bound variables to prevent free variables in v becoming bound after substitution.

FAILURE
SUBST1_TAC th (A,t) fails if the conclusion of th is not an equation. No change is made to the goal if no free occurrence of the left-hand side of th appears in t.
EXAMPLE
When trying to solve the goal
```   ?- m * n = (n * (m - 1)) + n
```
substituting with the commutative law for multiplication
```   SUBST1_TAC (SPECL ["m:num"; "n:num"] MULT_SYM)
```
results in the goal
```   ?- n * m = (n * (m - 1)) + n
```

USES
SUBST1_TAC is used when rewriting with a single theorem using tactics such as REWRITE_TAC is too expensive or would diverge. Applying SUBST1_TAC is also much faster than using rewriting tactics.
SEEALSO