Strong normalization property of CoC inside CoC Wikipedia says that


  The CoC is strongly normalizing, although, by Gödel's incompleteness
  theorem, it is impossible to prove this property within the CoC since
  it implies inconsistency.


Why is it impossible to prove within CoC that it is strongly normalizing?

Probably strong normalization property within CoC implies proof of consistency within CoC.  Then we can use the second Gödel's incompleteness theorem.  If so,

How does strong normalization property within CoC imply proof of consistency within Coc?

UPDATE:

In other words, why there can not exist a term of CoC that is a proof of CoC's proposition that CoC has normalization property. My guess is that such a term could be used to construct a term that proves a proposition of CoC that expresses consistency of CoC which is impossible by the second Gödel's incompleteness theorem.  How to construct a proof of consistency within CoC given a proof of normalization property?
I'll summarize the comments from chi, and sketch the proof that


There can be no proof of $\mathrm{False}:=\forall X:*.X$ in the CoC in head normal form. Furthermore, this fact can be proven in a weak theory, say Peano Arithmetic (though the excluded middle is not required).
This fact implies that if the CoC is normalizing, then it is consistent, and furthermore this implication does not use classical logic.


for 1., you proceed by induction on the term structure of a hypothetical closed term $t$ of type $\mathrm{False}$. Actually terms in normal form must be in the form:
 $$ \lambda x_1:T_1\ldots\lambda x_n:T_n.y\ t_1\ldots t_m$$

where $n$ and $m$ may be $0$. If $n$ is zero, then $t=y\ t_1\ldots t_m$, which is not possible since $t$ is closed (typed in the empty context). 

Otherwise, we may apply inversion and conclude that $T_1=*$ (and $x_1=X$), and we get
$$ X:*\vdash\lambda x_2\ldots\lambda x_n.y\ t_1\ldots t_m\ :\ X$$
to be derivable in the CoC. Now since $X$ is not a $\Pi$, we can apply inversion again to conclude that $n=1$ and in fact the above term is simply
$$ X:*\vdash y\ t_1\ldots t_m\ :\ X$$
Inversion yet again shows that
$$X:*\vdash y\ :\ \Pi y_1:U_1\ldots\Pi y_m:U_m.X $$
but $y$ must be $X$, since it is the only variable around! Therefore $m=0$, and $X=*$, which is impossible, contradiction.

Now all this reasoning is intuitionistic, as I've proven a negative (there can be no proof of...) and proofs of negations are always constructive. I do rely heavily on inversion, and you'll just have to take it on faith that this also can be proven in arithmetic, without the excluded middle, which is non-trivial.

Now for 2. we define consistency to mean "does not prove $\mathrm{False}$"! Again a negative statement. Now if the CoC is normalizing, one can take any normal form of a proof of $\mathrm{False}$ and use the above argument to get a contradiction. Again a constructive argument!

Finally to tie it all together. Now suppose you had enough arithmetic to carry out the above arguments in CoC. Note that this is almost possible: you actually need to add the axiom $0\neq 1$ to get anything off the ground. You can then prove that normalization implies consistency within the CoC, and you also have enough arithmetic for the second incompleteness theorem to apply. Therefore you cannot (if CoC is consistent!) prove normalization, as then you would have a full proof of consistency within CoC.