Contradiction between Gödel's Second Incompleteness Theorem and the Church-Rosser's property of CIC?
First, you are confusing consistency of CIC as an equational theory with consistency of CIC as a logical theory. The first means that not all terms of CIC (of the same type) are $\beta\eta$-equivalent. The second means that the type $\bot$ is not inhabited. CR implies the first kind of consistency, not the second.  This, as has been pointed out in the comments, is implied instead by (weak) normalization. The prototypical example of this situation is the pure $\lambda$-calculus: it is equationally consistent (CR holds) but, if you consider it as a logical system (as Alonzo Church orginally intended) it is inconsistent (indeed, it does not normalize).

Second, as Emil pointed out, even if CIC has a given property (CR or normalization) it is perfectly possible that CIC cannot itself prove that property. In this case, I do not see any inconsistency in the fact that CIC is able to prove its own CR property, and I guess that this is indeed the case (elementary combinatorial arguments usually suffice for CR, and such arguments definitely fall within the huge logical power of CIC).  However, CIC certainly does not prove its own normalization property, precisely because of the second incompleteness theorem.