Two functions currently perform
substitutions
in terms:
substitute and replace. Both take a term and a substitution as
arguments and produce a term, where a substitution
is a list of pairs, the first
element of which is a term representing the variable to be substituted for
and the second element of which is the term to substitute for that variable.
The function substitute will automatically rename bound variables in
order to avoid capture in the term during the substitution,
while the function
replace will perform a substitution without regard to capture.