DEFINITION pc3_t()
TYPE =
       ∀t2:T.∀c:C.∀t1:T.(pc3 c t1 t2)→∀t3:T.(pc3 c t2 t3)→(pc3 c t1 t3)
BODY =
Show proof