Proof of decidability of type checking of calculus of (co)inductive constructions? I often see it asserted that type checking is decidable for CIC, but I haven't seen it proven. Is there a good paper (or simple demonstration) of this?
I found another reference that goes through a detailed proof of the decidability of typechecking for systems of dependent types up to the CIC:

Chapter 2 of Advanced Topics in Types and Programming Languages: Dependent Types, David Aspinall &amp; Martin Hofmann.

As you probably know, the proof of decidability is conditional on decidability of $\beta$-equality, which itself is implied by the normalization of the calculus.

The proof of that statement is significantly more difficult, partly because it implies consistency of the logical system.