From Type Theory and Formal Proof, An Introduction by Rob Nederpelt and Herman Geuvers:
Definition 1.6.1 (Substitution)
(1a) $x[x := N] \equiv N$,
(1b) $y[x := N] \equiv y$ if $x \not \equiv y$,
(2) $(PQ)[x := N] \equiv (P[x := N])(Q[x := N])$,
(3) $(\lambda y . P)[x := N] \equiv \lambda z . (P^{y \to z} [x := N])$, if $\lambda z . P^{y \to z}$ is an $\alpha$-variant of $\lambda y . P$ such that $z \notin FV(N)$.
If I look at $(\lambda y . y)[y := a]$ then it seems that I can have either:
$(\lambda y . y)[y := a] = \lambda y . (y[y := a]) = \lambda y . a$
or
$(\lambda y . y)[y := a] = \lambda z . (z[y := a]) = \lambda z . z$
These are very different. Have I missed something in the definition?
Clearly, $\lambda y. a$ and $\lambda z.z$ are different (in the sense of not $\alpha$-equivalent) terms.
Actually, $(\lambda y. y)[y := a] = \lambda z. z = \lambda y. y\,$ (up to $\alpha$-equivalence) and there is no ambiguity. Indeed, according to definition 1.6.1 in Nederpelt' and Geuvers' handbook, $(\lambda y.y)[y:=a] \neq \lambda y.(y[y:=a])$ because in general $\lambda z . P^{y \to z}$ is defined provided that $z \notin FV(P)$ (see definition 1.5.1) and this condition does not hold in $\lambda y.y$ (where $z = y = P$).