DEFINITION csubc_gen_sort_l()
TYPE =
       ∀g:G.∀x:C.∀n:nat.(csubc g (CSort n) x)→(eq C x (CSort n))
BODY =
Show proof