The Proof Again

First, let us recall the definition of the collection of the types, Type.

Now the theorem:

The reduction can be lazy version , or eager version , or others. The actual meaning of the theorem is that computation on -terms respects type.

The proof of the theorem is by induction on , proceeding by cases on . The cases of 's being a variable or an abstraction is trivial, so the only case that need more concern is that t is an application . The proof in this case can be shown somewhat through the following figure, where triangles represent typing derivation trees.

>From above figure, first we have typing derivation tree which types to . Then, from application typing rule, we know is typed to for some type . Proceeding by induction, we know must also be typed to , thus we have a derivation tree for . Now abstraction typing rule tells us that must be typed to , which also means derivation tree for , , is a subtree of . Now a lemma is needed to show that and have the same type. Here is the lemma:

The lemma is easy to understand, and the proof to this lemma is by induction on the typing derivation , proceeding by cases on . For more detail, please see CN18 93.

By this lemma, we know is also in type . By induction hypothesis again, we know is of type , thus the proof is finished.