LP, the Larch Prover -- Substitutions

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

sigma(f(t1, ..., tn)) = f(sigma(t1), ..., sigma(tn))

A substitution sigma is an instance of a substitution sigma1 if there is a substitution sigma2 such that sigma(t) = sigma2(sigma1(t)).