DEFINITION pc3_pr2_u()
TYPE =
       ∀c:C.∀t2:T.∀t1:T.(pr2 c t1 t2)→∀t3:T.(pc3 c t2 t3)→(pc3 c t1 t3)
BODY =
        assume c: C
        assume t2: T
        assume t1: T
        suppose H: pr2 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
                   by (pr3_sing . . . H . H2)
                   we proved pr3 c t1 x
                   by (ex_intro2 . . . . previous H3)
                   we proved ex2 T λt:T.pr3 c t1 t λt:T.pr3 c t3 t
pc3 c t1 t3
          we proved pc3 c t1 t3
       we proved ∀c:C.∀t2:T.∀t1:T.(pr2 c t1 t2)→∀t3:T.(pc3 c t2 t3)→(pc3 c t1 t3)