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