CProp, since it was defined in CoRN as a Type, is predicative.

CProp, since it was defined in CoRN as a Type, is predicative.
However, it is not Type0, but a moving Type as usual, for example

  inductive and (A,B:CProp) : CProp := ...

  inductive exists (A:Type) (P:A->CProp) : CProp :=
   | ext : \forall x:A. \forall p : P x. exists A P.

does not pass since the sort of x is Type not included in CProp. Putting
exists in Type does not work either, if you want to make a conjuction
involving an existential.

solution, to be implemented:

  CProp of CicUniv.universe

where CProp n is meant to be Type (n + 0.5).