DEFINITION wcpr0_gen_sort()
TYPE =
       ∀x:C.∀n:nat.(wcpr0 (CSort n) x)→(eq C x (CSort n))
BODY =
Show proof