DEFINITION pc1_pr0_u2()
TYPE =
       ∀t0:T.∀t1:T.(pr0 t0 t1)→∀t2:T.(pc1 t0 t2)→(pc1 t1 t2)
BODY =
        assume t0: T
        assume t1: T
        suppose H: pr0 t0 t1
        assume t2: T
        suppose H0: pc1 t0 t2
          by (pc1_pr0_x . . H)
          we proved pc1 t1 t0
          by (pc1_t . . previous . H0)
          we proved pc1 t1 t2
       we proved ∀t0:T.∀t1:T.(pr0 t0 t1)→∀t2:T.(pc1 t0 t2)→(pc1 t1 t2)