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