I am reading Enderton's book, A mathematical introduction to logic, and I have a problem with the following lemma.
(Substitution Lemma, page 134) If the term $t$ is substitutable for the variable $x$ in the wff $\phi$ then $$\vDash_\mathfrak{A} \phi^x_t[s] \text{ iff } \vDash_\mathfrak{A} \phi[s(x|\overline s(t))].$$
He proceeds by induction on $\phi$, I only write the case where I have a trouble to understand it:
Case 4: $\phi = \forall y \psi$, and x does occur free in $\psi$. Because $t$ is substitutable for $x$ in $\phi$, we know that: (by the definition of "substitutable")
$y$ does not occur in $t$, and
$t$ is substitutable for $x$ in $\psi$.
By the $1.$ we have, $$\overline s(t) = \overline {s(y|d)}(t) \hspace{2cm}(*)$$ for any $d \in \mathfrak{|A|}$ . Since $x \neq y$, $\phi^x_t = \forall y \psi^x_t$.
$\vDash_\mathfrak{A} \phi^x_t[s]$ iff for every $d$, $\vDash_\mathfrak{A} \psi^x_t[s(y|d)]$, iff for every $d$, $\vDash_\mathfrak{A} \psi[s(y|d)(x|\overline s(t))]$ by the inductive hypothesis and $(*)$, iff $\phi[s(x|\overline s(t))]$.
I do not see why we need to use the fact $(*)$ in the second iff. I think that follows directly from inductive hypothesis.