DEFINITION pc3_pr2_r()
TYPE =
       ∀c:C.∀t1:T.∀t2:T.(pr2 c t1 t2)→(pc3 c t1 t2)
BODY =
        assume c: C
        assume t1: T
        assume t2: T
        suppose H: pr2 c t1 t2
          (h1) by (pr3_pr2 . . . H) we proved pr3 c t1 t2
          (h2) by (pr3_refl . .) we proved pr3 c t2 t2
          by (ex_intro2 . . . . h1 h2)
          we proved ex2 T λt:T.pr3 c t1 t λt:T.pr3 c t2 t
          that is equivalent to pc3 c t1 t2
       we proved ∀c:C.∀t1:T.∀t2:T.(pr2 c t1 t2)→(pc3 c t1 t2)