DEFINITION pr0_gen_sort()
TYPE =
       ∀x:T.∀n:nat.(pr0 (TSort n) x)→(eq T x (TSort n))
BODY =
Show proof