definition CProp0 : Type1 := Type0.
definition CProp1 : Type2 := Type1.
definition CProp2 : Type3 := Type2.
+definition CProp_of_CProp0: CProp0 → CProp ≝ λx.x.
+definition CProp_of_CProp1: CProp1 → CProp ≝ λx.x.
+definition CProp_of_CProp2: CProp2 → CProp ≝ λx.x.
+coercion CProp_of_CProp0.
+coercion CProp_of_CProp1.
+coercion CProp_of_CProp2.
inductive Or (A,B:CProp0) : CProp0 ≝
| Left : A → Or A B