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