What is the proof that the calculus of constructions, extended with recursive types (i.e., Fix at the type-level) isn't strongly normalizing?
With general recursive types you can define the type
type T = T -> T
With that type you can type self-application -- and in fact, every term of the untyped lambda calculus, including any of the well-known fixed-point operators. For example, the Y operator:
Y = \f:T. (\x:T. f (x x)) (\x:T. f (x x))
Here is a slightly more explicit version of what Andreas said.
The term $(\lambda x . x x) (\lambda x . x x)$ is not normalizing because it has exactly one $\beta$-redex, and when we reduce it we get back to the same term. But this term has the type $T$ for any type $T$ satisfying $T = T \to T$.