DEFINITION pc1_t()
TYPE =
       ∀t2:T.∀t1:T.(pc1 t1 t2)→∀t3:T.(pc1 t2 t3)→(pc1 t1 t3)
BODY =
Show proof