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