On Strong Normalization of the Calculus of Constructions with Type-Based Termination