Unification and substitutions in first-order logic I am currently learning about first-order logic and various resolution techniques. 
When applying a substitution $\theta$ to two sentences $\alpha$ and $\beta$, for unification purposes, aside from 
SUBST($\theta$, $\alpha$) = SUBST($\theta$, $\beta$), does the resulting substitution have to be unique? 
What I mean is, when unifying, when we check if SUBST($\theta$, $\alpha$) = SUBST($\theta$, $\beta$), is it OK if 
SUBST($\theta$, $\beta$) = $\beta$ ?
Thank you.

The most general unifier $\theta$ is unique in the sense that given any other unifier $\phi$, $\alpha \phi$ can be got from $\alpha \theta$ by a subtitution, and the same for $\beta$.
