I want to prove some theorems in lambda calculus using induction on the length of the term. Surprisingly, I haven't been able to find a single simple and complete proof online that uses this approach. Is the proof structure I have outlined below correct? I've read Induction on the length of a $\lambda$-term, but it didn't go into detail on the inductive step, which is the part I'm unsure about.
The base case for this type of proof is $lgh(M) = 1$. Proving the base case is simply proving that the theorem holds when $M$ is an atom.
For the inductive hypothesis, we assume that the theorem holds when $lgh(M) \lt n$.
Then we consider some $M$ where $lgh(M) = n$. By the syntax of lambda calculus, the term $M$ must be an atom, an application, or an abstraction. We've already handled the base case where $M$ is an atom. So now we have to consider the remaining two cases.
Case 1: $M$ is an application. Let $M \equiv P Q$. In proving this case, we can make use of the fact that since $lgh(P) < n$ and $lgh(Q) < n$, by the inductive hypothesis, the theorem holds for $P$ and $Q$.
Case 2: $M$ is an abstraction. Let $M \equiv λy.P$ In proving this case, we can make use of the fact that since $lgh(P) < n$, by the inductive hypothesis, the theorem holds for $P$.
Once we've proved the base case, and cases 1 and 2, the proof by induction is complete.
