`SUBS_CONV : thm list -> term -> thm`

SYNOPSIS
Substitution conversion.

DESCRIPTION
The call SUBS_CONV [th1; ...; th2] t, where the theorems in the list are all equations, will return the theorem |- t = t' where t' results from substituting any terms that are the same as the left-hand side of some thi with the corresponding right-hand side. Note that no matching or instantiation is done, in contrast to rewriting conversions.

FAILURE CONDITIONS
May fail if the theorems are not equational.

EXAMPLE
Here we substitute with a simplification theorem, but only instances that are the same as the LHS:
```  # SUBS_CONV[ARITH_RULE `x + 0 = x`] `(x + 0) + (y + 0) + (x + 0) + (0 + 0)`;;
val it : thm =
|- (x + 0) + (y + 0) + (x + 0) + 0 + 0 = x + (y + 0) + x + 0 + 0
```
By contrast, the analogous rewriting conversion will treat the variable x as universally quantified and replace more subterms by matching the LHS against them:
```  # REWRITE_CONV[ARITH_RULE `x + 0 = x`]
`(x + 0) + (y + 0) + (x + 0) + (0 + 0)`;;
val it : thm = |- (x + 0) + (y + 0) + (x + 0) + 0 + 0 = x + y + x
```