How do you formally show that “being a subterm of” is a transitive relation (on λ-terms)?

Question

I see in a book on Type Theory the following definition of a subterm of a $λ$-term:

We call $L$ a subterm of $M$ if $L ∈ \mathrm{Sub}(M)$.

• $\mathrm{Sub}(x) = \{x\}$, for each $x ∈ V. (V$ is the set of variables.)

• $\mathrm{Sub}(MN) = \mathrm{Sub}(M) ∪ \mathrm{Sub}(N) ∪ {MN}$.

• $\mathrm{Sub}(λx.M) = \mathrm{Sub}(M) ∪ {λx.M}$.

Well... it is as follows:

From the above definition, the properties below follow.

1. (Reflexivity) For all $λ$-terms $M$, we have $M ∈ \mathrm{Sub}(M)$.

2. (Transitivity) If $L ∈ \mathrm{Sub}(M)$ and $M ∈ \mathrm{Sub}(N)$, then $L ∈ \mathrm{Sub}(N)$.

Reflexivity is clear by definition, I think.

My question is how to prove transitivity.

I ask for help.

Answer 1

By induction on $N$, let us show that $\forall M\in\mathrm{Sub}(N)$, $\forall L\in\mathrm{Sub}(M)$, $L \in\mathrm{Sub}(N)$:

• If $N = x$ then $M = x$ and $L \in \mathrm{Sub}(M) = \mathrm{Sub}(N)$.
• If $N = λx.N'$, take $M\in\mathrm{Sub}(N)$. Either $M = N$ or $M \in \mathrm{Sub}(N')$.
  In the first case the result is immediate again: $L \in \mathrm{Sub}(M) = \mathrm{Sub}(N)$.
  In the second case, by induction you have $L \in \mathrm{Sub}(N') \subset \mathrm{Sub}(N)$.
• Similarly for the case of an application.

If it is not clear, please ask for details in the comments! :-)

Answer 2

The given definition allows us to conclude that M is a subterm of N if M "occurs" in N.

Therefore, we can say:

-- M is a subterm of M.

-- If L is a subterm of M and M is a subterm of N, then L is a subterm of N.

(I'm using as intuitive the notion of "M occurs in N".)