DEFINITION pr2_gen_sort()
TYPE =
       ∀c:C.∀x:T.∀n:nat.(pr2 c (TSort n) x)→(eq T x (TSort n))
BODY =
Show proof