In the literature there are several different proofs of Strong Normalization (SN) for the Calculus of Constructions (CC). Some of them are of purely syntactical nature (like the ones in [Coquand 1985],[Geuvers and Nederhof 1991] and in [Coquand and Gallier 1990]), while others give a proof of normalization by describing an appropriate semantics (like [Ong and Ritter 1994] and [Altenkirch 1993], who describe an denotationM semantics, but also [Goguen 1994], who describes a typed operational semantics). Apart from these, proofs of SN for CC can be found in [Berardi 1988],[Luo 1990](containing a proof of SN for the'Extended'Calculus of Constructions),[Terlouw 1993] and [Geuvers 1993](containing a proof of SN for CC with fl and r] reduction). Each of these proofs exploits the idea of interpreting types as specific sets of strongly normalizing A-terms. Then the terms are interpreted in such a way that,(1) if t is of type o', then the interpretation of t is in the set associated with~, and (2) for any term t, if its interpretation is SN, then t itself is SN. For systems without type dependency (like the potymorphic)~ calculus), it is rather well-known by now how to give a proof of SN using so called'saurated sets' as interpretations for the types. These saturated sets are sets of untyped,~ terms that satisfy some specific closure conditions and that are rather easy to work with. A possible drawback of this approach is that the interpretation of the typed term t should be an untyped term, and hence the interpretation will remove all type information from the term t (and hence it may remove some redexes). For the polymorphie,~ calculus, this is not a real problem, because the reduction that comes from type-abstractions a. nd type-applications can not be the source of an infinite reduction. In a system with type dependency, the situation is rather more complicated, because types can contain terms as subexpressions.(So, if one removes all types, then one also removes some terms.) In the Calculus of Constructions the situation is furthermore complicated by the fact that the system is higher order, which" means that there are reductions in type-constructors.