 Capture-avoiding first-order substitution

To perform a first-order substitution, first rename each conflicting bound variable to a fresh name, then replace the designated free occurrences. The fresh names must avoid the formula's relevant free names and all names in the inserted first-order term. For instance, substituting $f(u,t)$ for $z$ in $\exists tQ(z,t)$ requires renaming the binder, producing $\exists sQ(f(u,t),s)$ rather than $\exists tQ(f(u,t),t)$. The latter would change the intended meaning by capturing $t$.