DEFINITION pr1_t()
TYPE =
       ∀t2:T.∀t1:T.(pr1 t1 t2)→∀t3:T.(pr1 t2 t3)→(pr1 t1 t3)
BODY =
Show proof