I am beginning to study type theory, using Hindley's book "Simple Basic Type Theory", and I would like your help in proving a theorem. I would like to know if my idea of how to prove the theorem is correct or not, and if there are better / other ways to do it.

While learning about subject reduction and expansion I came across the following theorem:

**2C2. Subject expansion theorem** Yes $ Gamma vdash _ { lambda} Q: tau $ Y $ P vartriangleright _ { beta} Q $ for non-duplicating and non-canceling contractions, then

$ Gamma vdash _ { lambda} P: tau $.

The author leaves the test as an exercise and I am trying to do it. Here is my idea:

First, I wrote that it is enough to prove the theorem of a $ beta $-contraction (represented by $ vartriangleright_ {1 beta} $) From a $ beta $-reduction (represented by $ vartriangleright _ { beta} $) is simply zero or more steps of $ beta $-contraction.

Then I noticed that if $ P vartriangleright_ {1 beta} Q $ so $ P equiv ( lambda x.M) N $ Y $ Q equiv (N / x) M $. I also noticed that there must be exactly one occurrence of $ x $ free in $ M $, As the $ beta $ the contraction does not double and is not canceled. So, I tried an induction test on $ | P | $.

There are 3 cases:

*Case 1: $ M $ is a variable* In this case, since the contraction does not double or cancel, we must have $ M equiv x $. So, $ P equiv ( lambda x.x) N $ Y $ Q equiv N $. After the standard calculations, I was able to deduce the type of $ P $ as being $ tau $.

*Case 2: $ M $ It is an abstraction.* In this case $ P equiv ( lambda x. Lambda y. M_1) N $. So, $ Q equiv (N / x) ( lambda y. M_1) $. My idea here is to use the induction hypothesis to say that $ ( lambda x. M_1) N $ Y $ (N / x) M_1 $ must have the same type $ tau_1 $ and from there perform calculations to conclude that $ P $ Y $ Q $ must have the same type $ tau $.

*Case 3: $ M $ Is an application.* In this case $ P equiv ( lambda x. M_1 M_2) N $. There will only be one free occurrence of $ x $ in $ (M_1 M_2) $ and we consider only the case of this free occurrence in $ M_1 $. (because the other case is analogous). So, $ Q equiv (N / x) (M_1 M_2) = (((N / x) M_1) ((N / x) M_2)) = (((N / x) M_1) M_2) $. My idea is to use the induction hypothesis to say that $ ( lambda x. M_1) N $ Y $ (N / x) M_1 $ must have the same type $ tau_1 $ and then perform calculations to show that $ P $ Y $ Q $ must have the same type $ tau $.

Is my approach to the problem correct? Are there better / other ways to proceed?

Thanks in advance.