Trouble with a theorem in Hunter's Metalogic I'm a logician studian and I'm reading Hunter's Metalogic.
I'm having trouble understanding and exemplifing part of a theorem in the book.
It's the theorem 40.14, pp. 156-7.
40.14. Let t and u be terms. Let t' be the result of replacing each occurrence of vk in t by u. Let s be a sequence, and let u*s=d, i.e., let the member of D assigned by I to u for the sequence s be d. Let s' be s(d/k): i.e., let s' be the sequence that results from substituing d for the kth term of s. Then t's=ts': i.e. the member of D assigned by I to t' for the sequence s is the same as the member of D assigned by I to t for the sequence s'.
Proof (by induction):
Basis: n=1
There's 3 cases:


*

*$t$ is a constant;

*$t$ is a variable $v_j$ and $j$ is different from $k$

*$t$ is a variable $v_j$ and $j=k$.


Cases 1 and 3 are easy. But I cannot prove case 2, and also I cannot think of an example of it. Can anyone help?
Thanks!
 A: In your case 2, $t = v_j$ with $j \neq k$, the substitution of $u$ for $v_k$ has no effect on $t$!. So $t' = t$. 
But also, the sequence $s'$ equals the sequence $s$ except in the $k$th place. Now $v_j \ast s$ is the $j$th element of $s$, which is also the $j$th element of $s'$. 
Hence nothing changes and in this case $t' \ast s = t \ast s' = t \ast s$. 
A: The assignment function $s$ is a function :

$s : Var \to D$

where $Var$ is the set of variables : $v_1, v_2, v_3, \ldots, v_k, \ldots$, and $D$ is the domain of the interpretation $I$.
Assume a simple example with $D = \{ a, b, c, d, ... \}$ and let $s$ the following assignment :

$s(v_1)=a, s(v_2)=b, s(v_3)=c$ and $s(u)=d$.

Consider $s'=s[d/2]$, i.e. :

$s'(v_1)=a, s'(v_2)=d, s(v_3)=c$.

In this case, we have : $k=2$.
What happens if $t$ is $v_3$, i.e. $t$ is $v_j$ with $j=3$ and thus $j \ne k$ ? Clearly, $v_2$ does not occur in $t$; thus, the replacement of each occurrence of $v_2$ in $t$ by $u$ does not produce any change and $t'=t$. 
As you can see : $s'(v_3)=c=s(v_3)$ and thus $s'[t]=s'(v_3)=c=s(v_3)=s[t]=s[t']$.
