Is this proof of Barendregt's Substitution Lemma (lambda calculus) correct?

Question

So I have attempted to prove the lemma mentioned in the title, but I am not sure if it is correct. In the book I am reading, the Lemma was given without proof. We were given the following definitions:

Definition The set $\Lambda$ of all $\lambda$-terms

1. If $u \in V$, then $u \in \Lambda$

2. If $M$ and $N \in \Lambda$, then $(MN) \in \Lambda$

3. If $u \in V$ and $M \in \Lambda$, then $(\lambda u . M) \in \Lambda$

Alternatively, via abstract syntax

$$\Lambda = V \mid (\Lambda \Lambda) \mid (\lambda V . \Lambda)$$

and

Definition Substitution into $\lambda$-terms

1. $x[x := N] \equiv N$

2. $y[x := N] \equiv y$ if $x \not\equiv y$

3. $(PQ)[x := N] \equiv (P[x := N])(Q[x := N])$

4. $(\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 \not\in FV(N)$

Here is my attempted proof:

Lemma Let $x \not\equiv y$ and assume $x \not\in FV(L).$ Then: $$M[x:=N][y:=L] \equiv M[y := L][x := N[y := L]]$$

Proof. $M$ is a $\lambda$-term by definition. There are only three possible cases:

1. $M$ is a variable $z$.

   1. If $z \equiv x$ then \begin{aligned} M[x := N][y := L] &=\\\\ (x[x := N])[y := L] &=\\\\ N[y := L] \end{aligned} and \begin{aligned} M[y := L][x := N[y := L]] &=\\\\ (x[y := L])[x := N[y := L]] &=\\\\ x[x := N[y := L]] &=\\\\ N[y := L] \end{aligned}

   2. if $z \equiv y$ then \begin{aligned} M[x := N][y := L] &=\\\\ (y[x := N])[y := L] &=\\\\ y[y := L] &=\\\\ L \end{aligned} and \begin{aligned} M[y := L][x := N[y := L]] &=&\\\\ (y[y := L])[x := N[y := L]] &=& \\\\ L[x := N[y := L]] &=& \\\\ L &&\text{(since, per the Lemma, $x \not\in FV(L)$} \end{aligned}

   3. if $z \not\equiv x$ and $z \not\equiv y$ then trivially, both sides of the equation substitute to $z$.

2. $M \equiv (\lambda y . P)$ for some $P \in \Lambda$ In this case \begin{aligned} M[x := N][y := L] &=&\\\\ (\lambda y . P)[x := N][y := L] &=&\\\\ (\lambda u . P^{y \to u} [x := N])[y := L] &=&\\\\ (\lambda u . P^{y \to u} [x := N][y := L]) &,& u \not\in FV(N) \cup FV(L) \end{aligned} and similarly \begin{aligned} M[y := L][x := N[y := L]] &=&\\\\ (\lambda y . P)[y := L][x := N[y := L]] &=&\\\\ (\lambda u . P^{y \to u} [y := L][x := N[y := L]]) &,& u \not\in FV(N) \cup FV(L) \end{aligned}

   Therefore, if $$P^{y \to u} [x := N][y := L] \equiv P^{y \to u} [y := L][x := N[y := L]]$$ then $$(\lambda y . P)[x := N][y := L] \equiv (\lambda y . P) [y := L][x := N[y := L]]$$

3. $M \equiv P Q$ for some $P, Q \in \Lambda$ In this case $$M[x := N][y := L] = (P[x := N][y := L])(Q[x := N][y := L])$$ and $$\begin{gathered} M[y := L][x := N[y := L]] =\\\\ (P[y := L][x := N[y := L]])(Q[y := L][x := N[y := L]]) \end{gathered}$$

   Therefore if $$P[x := N][y := L] = P[y := L][x := N[y := L]]$$ and $$Q[x := N][y := L] = Q[y := L][x := N[y := L]]$$ then $$PQ[x := N][y := L] = PQ[y := L][x := N[y := L]]$$

Using case $1$ as the base case, we've proved the lemma by induction using $2$ and $3$

Something doesn't feel right about this. I feel as though I didn't link the first case with the second two cases strongly enough to be able to invoke induction, or did I? I would also appreciate any advice on how to make the proof better.

Answer 1

Your proof is fine. Maybe it's a little too verbose, but it's just a matter of style, not of correctness.

The point is that the proof is by structural induction on the term $M$ (in general, this is written at the beginning of the proof, not at the end).

The base case is when $M$ is a variable, and for the base case you don't need the induction hypothesis, as usual.

In the application ($M \equiv PQ$) and abstraction ($M \equiv \lambda x.P$) cases, you need the induction hypothesis (that is, $P [x := N] [y := L] = P[y := L][x := N[y := L]]$ and, for the application case, $Q [x := N] [y := L] = Q[y := L][x := N[y := L]]$ too) to conclude.

The link between the variable case and the abstraction or application case is implicit (as usual in a proof by structural induction), you don't have to write anything else. Where is this implicit link? Think of the "simplest" application. It is an application of the form $M \equiv z_1z_2$ (possibly $z_1 \equiv z_2$). So, according to your (correct) proof, in the application case the induction hypothesis says that $z_1 [x := N] [y := L] = z_1[y := L][x := N[y := L]]$ and $z_2 [x := N] [y := L] = z_2 [y := L][x := N[y := L]]$. We know from the base case that actually the induction hypothesis is true, hence you know that $(z_1z_2) [x := N] [y := L] = (z_1z_2)[y := L][x := N[y := L]]$ is true, and now you can go on with more complex terms (an analogous argument holds for the "simplest" abstraction, $M = \lambda z_1.z_2$).