Understanding the Proof of Strong Normalization of the Calculus of Constructions
Unfortunately, I'm not sure there are more beginner friendly resources than Geuvers' account. You might try this note from Chris Casinghino which gives an account of several proofs in excruciating detail.

I'm not sure I understand the gist of your confusion, but I think one important thing to note, is the following lemma (Corollary 5.2.14), proven in the classic Barendregt text:

$$\Gamma \vdash M:T\ \Rightarrow\ \Gamma \vdash T:*\mbox{ or }\square $$

This means that while $[\![T]\!]_\xi$ can be some complicated function, if $\Gamma \vdash M:T$ holds, then $[\![T]\!]_\xi$ has to be a set of terms.

This is insinuated in the outline (section 3.1), where $(\!|t|\!)_\sigma\in[\![T]\!]_\xi$ only if $\Gamma \vdash t:T :*$, which lines up with our expectation, which is that the interpretation of a type must be a set of terms, i.e. ${\cal V}(*)\subseteq{\cal P}(\mathrm{Term})$ (indeed, ${\cal V}(*)=\mathrm{SAT}$!)

It's a common situation in type theory that even though we're only interested in the "base kind" (here $*$), we still have to define semantics for things at higher kinds (hence the need to introduce $\mathrm{SAT}^*$). Things then work out at the end, because only kind which inhabited by types is $*$ (and $\square$, but that's not really important).