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?
What is a proof of normalization of Morte?
type theory;functional programming;turing completeness