What is a proof of normalization of Morte?

It is said that any term on the calculus of construction halts. I am studying it through Morte, which is a bare bone implementation of the coc available on github. Is there any simple proof of normalization for the calculus of constructions? If the proof isn't simple, is there an simple intuition behind the result?

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$.

StackExchange Computer Science Q#49393, answer score: 2