Comment by 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.