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