I'm going through "Type Theory and Formal Proof" by Nederpelt and Geuvers and just trying to play around with $\lambda\underline\omega$ after reading the chapter on it to better grasp the material. The text is a bit vague on some formalities, so I have a couple of questions.
Consider the term $t = \lambda x : ((\lambda \alpha : *. \alpha) nat). x$ (assuming $nat : *$ is in context). Can type-level abstractions and applications be used like this under lambda abstraction type annotations? So, is $t$ a valid term?
If it is, then clearly its type is $(\lambda \alpha : *. \alpha) nat \rightarrow (\lambda \alpha : *. \alpha) nat$, which is $\beta$-equivalent to $nat \rightarrow nat$. But how does $t$ relate to $\lambda x:nat.x$? In other words, can $\beta$-reduction be done under the lambda abstraction type annotation?