Substitution identities: $\mu(x/ \sigma)(y/\tau) = \mu(x/ \sigma, y/\tau) = \mu(y/\tau)(x/\sigma)$ If $x$ and $y$ are distinct variables, $\sigma$ and $\tau$ closed $M$-terms, and $\mu$ is any
$M$-term, how can I show that $\mu(x/ \sigma)(y/\tau) = \mu(x/ \sigma, y/\tau) = \mu(y/\tau)(x/\sigma)$ ? 
I tried to prove it by induction and permuting but I think it is a wrong way.
The definitions of this elements are given in "the incompleteness phenomenon" which is a Haim Judah's book
Let $\cal{L}$ be a language, $\cal{M}$ a model for $\cal{L}$
$\tau$ is an M-term if one of the following conditions hold:
(i) $\tau$ is a constant in the language $\cal{L}$
(ii) $\tau$ is a variable.
(iii) there is an n-ary function symbol F in $\cal{L}$ and M-terms
 $\tau_1$, ... ,  $\tau_n$ such that  $\tau = F( \tau_1, ... ,  \tau_n)$
(iv) $\tau$ is an element of M.
Thus, M-terms are defined like terms, but we also allow elements of the universe of $\cal{M}$ to be used as blocks.
an M-term is closed if it does not contain any variables.
I have proved the case $\tau$ constant, $\tau$ variable, but the third one I don't know to do it
 A: For $\mu$ an $\mathcal M$-term from cases $\rm(i)$ and $\rm(iv)$, we observe that $x$ nor $y$ occurs in $\mu$, so that $$\mu = \mu(x/\sigma)(y/\tau)=\mu(x/\sigma,y/\tau)=\mu(y/\tau)(x/\sigma)$$
Likewise for $\mu$ a variable that is not $x$ or $y$. If $\mu = x$, then:


*

*$\mu(y/\tau) = \mu$, so $\mu(y/\tau)(x/\sigma) = \sigma$;

*$\mu(x/\sigma) = \sigma$, and $y$ does not occur in $\sigma$, so $\sigma(y/\tau)=\sigma$. Hence $\mu(x/\sigma)(y/\tau) = \sigma$;

*$\mu(x/\sigma,y/\tau)=\sigma$


Mutatis mutandis, we deal with $\mu = y$. This concludes case $\rm(iii)$ in our proof by structural induction.
Finally, we turn to $\rm(iv)$, which is the only "inductive" clause. The result will follow from the lemma that:
$$F(\tau_1,\ldots,\tau_n)\,(\vec x/\vec\sigma) = F(\tau_1(\vec x/\vec\sigma),\ldots,\tau_n(\vec x/\vec\sigma))$$
(after which the induction hypothesis can be applied to each of $\tau_1,\ldots, \tau_n$). Depending on the desired level of formality and the definitions used, this lemma can be:


*

*dismissed/glossed over as "obvious";

*justified by saying "each variable in $F(\dots)$ must occur in one of the $\tau_i$";

*proved meticulously by unfolding the definition of substitution;

*the definition of substitution itself, for terms of the form $F(\dots)$.


Since most books/notes don't bother to give a very rigorous definition of "substitution" beyond "replacing all occurrences", I suspect that the second bullet is most suited to your situation.
