DEFINITION pc3_t()
TYPE =
       ∀t2:T.∀c:C.∀t1:T.(pc3 c t1 t2)→∀t3:T.(pc3 c t2 t3)→(pc3 c t1 t3)
BODY =
        assume t2: T
        assume c: C
        assume t1: T
        suppose H: pc3 c t1 t2
        assume t3: T
        suppose H0: pc3 c t2 t3
          (H1) consider H0
          consider H1
          we proved pc3 c t2 t3
          that is equivalent to ex2 T λt:T.pr3 c t2 t λt:T.pr3 c t3 t
          we proceed by induction on the previous result to prove pc3 c t1 t3
             case ex_intro2 : x:T H2:pr3 c t2 x H3:pr3 c t3 x ⇒
                the thesis becomes pc3 c t1 t3
                   (H4) consider H
                   consider H4
                   we proved pc3 c t1 t2
                   that is equivalent to ex2 T λt:T.pr3 c t1 t λt:T.pr3 c t2 t
                   we proceed by induction on the previous result to prove pc3 c t1 t3
                      case ex_intro2 : x0:T H5:pr3 c t1 x0 H6:pr3 c t2 x0 ⇒
                         the thesis becomes pc3 c t1 t3
                            by (pr3_confluence . . . H6 . H2)
                            we proved ex2 T λt:T.pr3 c x0 t λt:T.pr3 c x t
                            we proceed by induction on the previous result to prove pc3 c t1 t3
                               case ex_intro2 : x1:T H7:pr3 c x0 x1 H8:pr3 c x x1 ⇒
                                  the thesis becomes pc3 c t1 t3
                                     (h1) by (pr3_t . . . H5 . H7) we proved pr3 c t1 x1
                                     (h2) by (pr3_t . . . H3 . H8) we proved pr3 c t3 x1
                                     by (pc3_pr3_t . . . h1 . h2)
pc3 c t1 t3
pc3 c t1 t3
pc3 c t1 t3
          we proved pc3 c t1 t3
       we proved ∀t2:T.∀c:C.∀t1:T.(pc3 c t1 t2)→∀t3:T.(pc3 c t2 t3)→(pc3 c t1 t3)