A substitution is a mapping from variables to
terms (of the appropriate sorts). A substitution
can be applied to a term as well as to a variable; its effect is to replace
(simultaneously) each variable in the term by the substitution applied to that
variable. More precisely, if sigma is a substitution defined on
variables, then sigma extends to terms by setting