Enderton's Lemma 25B, $\overline s(u^{x}_{t})=\overline {s(x|\overline s(t))}(u)$ I am reading Enderton's book, A mathematical introduction to logic, and I have a problem with the following lemma (page 133, Lemma 25B).

Consider a fixed structure $\mathfrak{A}$ and $s: V \rightarrow |\mathfrak{A}|$ , where $V$ is set of variables. Suppose that $u, t$ are terms and $x$ is a variable. Then
$$\overline s(u^{x}_{t})=\overline {s(x|\overline s(t))}(u).$$

He outlined the proof by induction on the term $u$. Thus, I write out the details, but I have a problem in the base case if we consider that $u$ is some variable.

The funtion $s(x|d)(y)$ is defined as follows:
$\begin{align}
s(x|d)(y) = 
\begin{cases}
s(y) &\text{if } y \neq d, 
\\ \\
d &\text{if } y = d.
\end{cases}
\end{align}$
(base case) Let $u$ be some variable. We consider two cases:

*

*$u \neq x;$ we have $u^{x}_{t} = u$. Thus, $\overline s(u^{x}_{t}) = \overline s(u)$. On the other hand, since $u$ is a variable, i.e., $u$ is atomic, we have by the definition $\overline  {s(x|\overline s(t))}(u) = {s(x|\overline s(t))}(u)$. If $\overline s(t) \neq u$, then ${s(x|\overline s(t))}(u) = s(u) = \overline s(u)$, otherwise ${s(x|\overline s(t))}(u) = \overline s(t) = u$. Clearly, $\overline s(u) \neq u$.

Maybe, since the value of $\overline s(t)$ is in $\mathfrak{A}$ and $u$ is just variable we can conclude that the case $\overline s(t) = u$ never happen. Thus, the case holds. Am I right?

*

*$u = x$; have a similar problem.


It's been a while since I've read the book and I don't have it with me, so I'm not sure exactly where the overlines go. I'll just skip them entirely; they aren't all that important to the question. (It's very good that you're careful with them though!)
In the case you discuss, $s(x|s(t))(u) = s(u)$ because $u \neq x$, by the first clause of the definition you give. You don't care what $s(u)$ and $s(t)$ are.
In the other case, u=x so
$$s(u^x_t) = s(t) = s(x|s(t))(x) = s(x|s(t))(u)$$
The last equality holds by the second clause of your definition (because $u=x$). 
