On one hand, Gödel's Second Incompleteness Theorem states that any consistent formal theory that is strong enough to express any basic arithmetical statements can't prove its own consistency. On the other hand, the Church-Rosser's property of a formal (rewriting) system tells us that it is consistent, in the sense that not all equations are derivable, for example, K$\neq$I, since they don't have the same normal form.
Then the Calculus of Inductive Constructions (CIC) clearly statisfies both conditions. It is strong enough to represent arithmetical propositions (indeed, the $\lambda\beta\eta$-calculus alone is already able to encode the Church numerals and represent all primitive recursive functions). Moreover, CIC also has the confluence or Church-Rosser property. But:
shouldn't CIC be unable to prove its own consistency by the Second Incompleteness theorem?
Or it just states that the CIC can't prove its own consistency inside the system, and somehow the confluence property is a meta-theorem? Or maybe the confluence property of CIC does not guarantee its consistency?
I would highly appreciate if someone could shed some light on those issues!