where
are the closed
-terms.
Proof by induction on , by cases on
.
case is a variable:
This case does not apply since is closed.
case is an abstraction
:
since abstractions evaluate
to themselves, so
.
case is an application
:
(or else the computation can't
continue).
From the application typing rule, we know that
,
therefore, proceeding by induction, .
Now .
We know from the abstraction typing rule that
and
.
Thus, using the lemma shown in the next lecture,
we conclude that .
QED.