I have difficulties in understanding the proof of strong normalization for the calculus of constructions. I try to follow the proof in the paper of Herman Geuvers "A short and flexible proof of Strong Normalization for the Calculus of Constructions".
I can follow the main line of reasoning well. Geuvers constructs for each type $T$ an interpretation $[\![T]\!]_\xi$ based on some evaluation of type variables $\xi(\alpha)$. And then he constructs some term interpretation $(\!|M|\!)_\rho$ based on some evaluation of term variables $\rho(x)$ and proves that for valid evaluations the assertion $(\!|M|\!)_\rho \in [\![T]\!]_\xi$ for all $\Gamma\vdash M:T$ holds.
My problem: For easy types (like system F types) the type interpretation $[\![T]\!]_\xi$ is really a set of terms, so the assertion $(\!|M|\!)_\rho \in [\![T]\!]_\xi$ makes sense. But for more complex types the interpretation $[\![T]\!]_\xi$ is not a set of terms but a set of functions of some appropriate function space. I think, I almost understand the construction of the function spaces, however it cannot assign any meaning to $(\!|M|\!)_\rho \in [\![T]\!]_\xi$ for the more complex types $T$.
Can anybody explain or give links to some more understandable presentations of the proof?
Edit: Let me try to make the question clearer. A context $\Gamma$ has declarations for type variables $\alpha:A$ and object variables. A type valuation is valid, if for all $(\alpha:A) \in \Gamma$ with $\Gamma\vdash A:\square$ then $\xi(\alpha) \in \nu(A)$ is valid. But $\nu(A)$ can be an element of $(SAT)^*$ and not only $SAT$. Therefore no valid term evaluation can be defined for $\rho(\alpha)$. $\rho(\alpha)$ must be a term and not some function of a function space.
Edit 2: Example which does not work
Let's make the following valid derivation: $$ \begin{array}{llll} [] &\vdash & *:\square &\text{axiom} \\ [\alpha:*] &\vdash& \alpha:* &\text{variable introduction} \\ [\alpha:*] &\vdash& *:\square &\text{weaken} \\ [] &\vdash & (\Pi \alpha:*.*):\square &\text{product formation} \\ [\beta:\Pi \alpha:*.*] &\vdash& \beta:(\Pi \alpha:*.*) &\text{variable introduction} \end{array} $$
In the last context a valid type evaluation must satisfy $\xi(\beta) \in \nu(\Pi \alpha:*.*) = \{f| f:\text{SAT} \to \text{SAT}\}$. For this type evaluation there is no valid term evaluation.