DEFINITION pc3_gen_sort()
TYPE =
       ∀c:C.∀m:nat.∀n:nat.(pc3 c (TSort m) (TSort n))→(eq nat m n)
BODY =
Show proof