----------------------------------------------------------------------
subst                                                           (Term)
----------------------------------------------------------------------
subst : (term,term) subst -> term -> term

SYNOPSIS
Substitutes terms in a term.

DESCRIBE
Given a "(term,term) subst" (a list of {{redex, residue}} records) and a
term {tm}, {subst} attempts to replace each free occurrence of a
{redex} in {tm} by its associated {residue}. The substitution is done in
parallel, i.e., once a redex has been replaced by its residue, at some
place in the term, that residue at that place will not itself be
replaced in the current call. When necessary, renaming of bound
variables in {tm} is done to avoid capturing the free variables of an
incoming residue.

FAILURE
Failure occurs if there exists a {{redex, residue}} record in the
substitution such that the types of the {redex} and {residue} are not
equal.

EXAMPLE

- load "arithmeticTheory";

- subst [Term`SUC 0` |-> Term`1`]
        (Term`SUC(SUC 0)`);
> val it = `SUC 1` : term

- subst [Term`SUC 0` |-> Term`1`,
         Term`SUC 1` |-> Term`2`]
        (Term`SUC(SUC 0)`);
> val it = `SUC 1` : term

- subst [Term`SUC 0` |-> Term`1`,
         Term`SUC 1` |-> Term`2`]
        (Term`SUC(SUC 0) = SUC 1`);
> val it = `SUC 1 = 2` : term

- subst [Term`b:num` |-> Term`a:num`]
        (Term`\a:num. b:num`);
> val it = `\a'. a` : term

- subst [Term`flip:'a` |-> Term`foo:'a`]
        (Term`waddle:'a`);
> val it = `waddle` : term




SEEALSO
Term.inst, Thm.SUBST, Drule.SUBS, Lib.|->.

----------------------------------------------------------------------