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