DEFINITION pr3_pr1()
TYPE =
∀
t1:
T
.
∀
t2:
T
.(
pr1
t1 t2)
→
∀
c:
C
.(
pr3
c t1 t2)
BODY =
Show proof