Barendregt  introduces the following two definitions of substitution and their equivalence:
Ottamnn variable convention (p. 26)
2.1.13. Ottamnn variable convention. If $M_1, ..., M_n$ occur in a certain mathematical context (e.g. definition, proof), then in these terms all bound variables are chosen to be different from the free variables.
Remark 1: I'm using the name 'Ottmann variable convention' because in the 6th impression of "The Lambda Calculus. Its Syntax and Semantics", Barendregt replaced the name 'variable convention' by this name. See 'Addenda for the sixth imprinting', p. E1.
Equivalence (p. 579)
If one observes the variable convention, then $M[ x:= N ]$ as in definition 2.1.15 is the same substitution as in Curry's definition C.1.
Since (1) follows the Ottmann variable convention its normalisation using both definitions of substitution should be the same.
$$(λxx.x)yz \qquad \qquad (1)$$
Remark 2: I know it is silly to abstract over $x$ twice in (1), but this is not banned anywhere.
Using Definition C.1, the normalisation of (1) is $z$, but using Definition 2.1.15 I got stuck in
$$(λxx.x)yz = ((λx.x)[ x:=y ])z$$
because Definition 2.1.15 doesn't include a clause when the bound variable and the variable to substitute are the same, that is, the missing clause is
$$λx.M[ x:=N ] ≡ λx.M.$$
Are really both definitions the same using the Ottmann variable convention? Am I missing something when using Definition 2.1.15?
Barendregt, H. P. (2004). The Lambda Calculus. Its Syntax and Semantics. Revised edition, 6th impression. Vol. 103. Studies in Logic and the Foundations of Mathematics. Elsevier.