What is a proof of normalization of Morte?
I'm afraid there is no simple proof of the normalization for the CoC, as it implies the consistency of a very strong form of logic.

A good reference is Geuvers, A short and flexible proof of strong normalization for the calculus of constructions.

The intuition of the proof is hard to convey, but basically it is shown that for each type $T$, there exists a notion of "term computable at type $T$", which is a predicate, intuitively a subset of the set of $\lambda$-terms. A computable term has good properties, in particular it is always normalizing. Building this notion of computability involves building a kind of model for the CoC, often called a realizability model.

Then it is shown that any well typed term $t:T$ is computable at type $T$.