[perthmad]

What do you mean? CoC definitely supports impredicative encodings, and as far as expressivity goes, this allows to implement a lot of programs. Proving them correct is another matter, but that's not what you implied. Also, CIC is notably not Turing-complete.

[logicchains]

I was referring to https://link.springer.com/chapter/10.1007/3-540-45413-6_16; induction is not derivable in pure CoC. I suppose yes technically you could base a dependently-typed language on it if you didn't mind not supporting induction, but I can't imagine many people wanting to use it, as it would be quite limited compared to one supporting inductive proofs. Or at least when people think of "dependently typed programming language", they're usually thinking of something at least as expressive as CIC.