I am going through the book on lambda calculus by Hindley and Seldin . They introduce the syntactic equivalence of expressions and proving them by a technique named "induction" , which has not been directly defined in the book .
(a) $[N/x]x \equiv N$
(b) $[N/x]a \equiv a$ for all atoms $a \not \equiv x$
(c) $[N/x](PQ) \equiv ([N/x]P)([N/x]Q)$
(d) $[N/x](\lambda x.P) \equiv (\lambda x.P)$
(e) $[N/x](\lambda y.P) \equiv P$ if $x \not \in FV(P)$.
(f) $[N/x](\lambda y.P) \equiv \lambda y. [N/x]P$ if $x \in FV(P)$ and $y \not \in FV(N)$.
(g) $[N/x](\lambda y.P) \equiv \lambda z. [N/x][z/y]P$ if $x \in FV(P)$ and $y \in FV(N)$.
The above are the rules given for substitution in the book. I have some difficulty in understanding (d).
Why is it so that $$ [N/x] ( \lambda x . p) = ( \lambda x . p) $$ ? How to justify this ? Why can't this be defined to be or equal to $$( \lambda N . p) $$ ?