Prove that $[x/x] M \equiv M$

Question

I just started reading the book Lambda-Calculus and Combinators An Introduction. Using this definition of Substitution in Page 7.

I want to prove that if $M$ is any term $[x/x] M \equiv M$. In the book it is given that proof follows by checking the clauses in the definition. I can't see any formal proof from that. I think that it requires induction on M. Any hints?

Answer 1

I am pasting the answer which Aleš Bizjac left in a comment.

Yes, it requires induction on $M$ and then in each case you check the corresponding clauses of the definition. You are proving a statement $∀M∈T,∀x∈V,[x/x]M=M$, where $T$ is the set of lambda terms and $V$ is the set of variables. The set of lambda terms is defined inductively therefore you can use structural induction. Then for instance in the case of application $M=PQ$ you can assume that $[x/x]P=P$ and $[x/x]Q=Q$ since $P$ and $Q$ are subterms of $M$.