DEFINITION ty3_gen_sort()
TYPE =
       ∀g:G.∀c:C.∀x:T.∀n:nat.(ty3 g c (TSort n) x)→(pc3 c (TSort (next g n)) x)
BODY =
Show proof