Proof that the calculus of constructions extended with recursive types isn't strongly normalizing? 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 -&gt; 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))