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