Lambda the Ultimate

This is the calculus introduced in the "Safe Type-level Abstractions in Scala" paper, and also used in "Generics of a Higher Kind." When I read the latter paper I saw something confusing, and just today I re-read the earlier paper to confirm that it contains the same thing.

In the rules for type expansion (Figure 7 in the paper I linked above), in the X_SEL case, one of the premises is (excuse my attempt to format this with ASCII):

Gamma |- [x -> T]S << R

From what I understand, x is a term-level variable, and T is a type. How can that substitution work, then? Wouldn't the result be syntactically invalid?

I wouldn't be surprised if I am missing some detail in the paper, so if anybody with a better understanding could point me in the right direction, I'd appreciate it.

Edit:
Thinking about it a bit, it seems like the premise ought to be, instead:

Gamma, x : T |- S << R