Lambda the Ultimate

If this sounds like a worthy goal, or if you are simply interested in the use of proof assistants for rogramming language research, you don't want to miss upcoming tutorial.

Hi,
I read the proof of the weak normalisation theorem on the book Proofs and Types, on the chapter 4.

There is something that seems strange to me.

It says that:

The degree &(T) of a type is defined by:
- &(T_i) = 1 if T_i is atomic.
- &(U x V) = &(U -> V) = max(&(U), &(V)) + 1

The degree &(r) of a redex is defined by:
- &(fst) = &(snd) = &(U x V) where U x V is the type of
- &((\x.v)u) = &(U -> V) where U -> V is the type of (\x.v)

Reading this it seems to me that a redex has the degree of its type. Am I wrong?

Anyway, after it says:

Note that, if r is a redex of type T, then &(r) > &(T).

Why should &(r) be greater than &(T)?

thanks,
bye