DEFINITION pr2_gen_csort()
TYPE =
       ∀t1:T.∀t2:T.∀n:nat.(pr2 (CSort n) t1 t2)→(pr0 t1 t2)
BODY =
Show proof