 First-order substitution

Replacing every free occurrence of variable $z$ in a first-order formula by a first-order term $\tau$. Bound occurrences of $z$ are left alone. The operation requires either that $\tau$ be free for substitution at those occurrences or that conflicting bound variables first be renamed, as in capture-avoiding first-order substitution.