DEFINITION pc1_pr0_x()
TYPE =
       ∀t1:T.∀t2:T.(pr0 t2 t1)→(pc1 t1 t2)
BODY =
        assume t1: T
        assume t2: T
        suppose H: pr0 t2 t1
          (h1) by (pr1_refl .) we proved pr1 t1 t1
          (h2) by (pr1_pr0 . . H) we proved pr1 t2 t1
          by (ex_intro2 . . . . h1 h2)
          we proved ex2 T λt:T.pr1 t1 t λt:T.pr1 t2 t
          that is equivalent to pc1 t1 t2
       we proved ∀t1:T.∀t2:T.(pr0 t2 t1)→(pc1 t1 t2)