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