I have been playing around with $\lambda$ calculus. This is a superb invention, I really think it is the most concise mechanism for modelling computation, it is the most compact and smallest programming language ever. In my mind, the inventor  of this calculus, Alonso Church should be more celebrated than his famous student Alan Turing. I am serious. It is a neat system and quite a lot of fun. That seems odd considering it is now about 80 years old.

Anyway I have been studying this and in Barendregt and Barendsen’s introduction to the subject, there is Exercise 2.2 where we are asked to prove the substitution lemma, namely

$M[x:=N][y:L] \equiv M[y:L][x:=N[y:=L]]$, with $x \not \equiv y, x \not \in FV(L)$

I have no short cut way of proving this. I can prove it by doing an induction on the complexity of $M$, see Definition 2.4, iii) with specially using the induction hypothesis for cases  $(M_1M_2), \lambda y.M_1$. Of course with the use of the side conditions too.

Likewise I could not see the use of Exercise 2.2 to prove Exercise 2.3. If you can, show me please your proof.

However, I can prove both items in Exercise 2.3 using my long method. For example, for the case of Exercise 2.3, ii, I would use the same method on the complexity of $M, M'$ respectively and thus prove $\lambda \vdash M = M' \wedge \lambda \vdash N = N' \Rightarrow \lambda \vdash M[x:=N] = M'[x:=N']$.

Yeah, I changed the notation from subscripts to primes so that it gets clearer when dealing with Definition 2.4, iii.

Hope this helps and if you have a short cut way, let me know. Thanks.

LPC