DEFINITION sty0_gen_sort()
TYPE =
       ∀g:G.∀c:C.∀x:T.∀n:nat.(sty0 g c (TSort n) x)→(eq T x (TSort (next g n)))
BODY =
Show proof