DEFINITION pr3_pr2()
TYPE =
       ∀c:C.∀t1:T.∀t2:T.(pr2 c t1 t2)→(pr3 c t1 t2)
BODY =
        assume c: C
        assume t1: T
        assume t2: T
        suppose H: pr2 c t1 t2
          by (pr3_refl . .)
          we proved pr3 c t2 t2
          by (pr3_sing . . . H . previous)
          we proved pr3 c t1 t2
       we proved ∀c:C.∀t1:T.∀t2:T.(pr2 c t1 t2)→(pr3 c t1 t2)