DEFINITION pc3_pc1()
TYPE =
       ∀t1:T.∀t2:T.(pc1 t1 t2)→∀c:C.(pc3 c t1 t2)
BODY =
        assume t1: T
        assume t2: T
        suppose H: pc1 t1 t2
        assume c: C
          (H0) consider H
          consider H0
          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 pc3 c t1 t2
             case ex_intro2 : x:T H1:pr1 t1 x H2:pr1 t2 x ⇒
                the thesis becomes pc3 c t1 t2
                   (h1) by (pr3_pr1 . . H1 .) we proved pr3 c t1 x
                   (h2) by (pr3_pr1 . . H2 .) we proved pr3 c t2 x
                   by (ex_intro2 . . . . h1 h2)
                   we proved ex2 T λt:T.pr3 c t1 t λt:T.pr3 c t2 t
pc3 c t1 t2
          we proved pc3 c t1 t2
       we proved ∀t1:T.∀t2:T.(pc1 t1 t2)→∀c:C.(pc3 c t1 t2)