DEFINITION ty3_sconv_pc3()
TYPE =
       ∀g:G.∀c:C.∀u1:T.∀t1:T.(ty3 g c u1 t1)→∀u2:T.∀t2:T.(ty3 g c u2 t2)→(pc3 c u1 u2)→(pc3 c t1 t2)
BODY =
        assume g: G
        assume c: C
        assume u1: T
        assume t1: T
        suppose H: ty3 g c u1 t1
        assume u2: T
        assume t2: T
        suppose H0: ty3 g c u2 t2
        suppose H1: pc3 c u1 u2
          (H2) consider H1
          consider H2
          we proved pc3 c u1 u2
          that is equivalent to ex2 T λt:T.pr3 c u1 t λt:T.pr3 c u2 t
          we proceed by induction on the previous result to prove pc3 c t1 t2
             case ex_intro2 : x:T H3:pr3 c u1 x H4:pr3 c u2 x ⇒
                the thesis becomes pc3 c t1 t2
                   (H_y) by (ty3_sred_pr3 . . . H4 . . H0) we proved ty3 g c x t2
                   (H_y0) by (ty3_sred_pr3 . . . H3 . . H) we proved ty3 g c x t1
                   by (ty3_unique . . . . H_y0 . H_y)
pc3 c t1 t2
          we proved pc3 c t1 t2
       we proved ∀g:G.∀c:C.∀u1:T.∀t1:T.(ty3 g c u1 t1)→∀u2:T.∀t2:T.(ty3 g c u2 t2)→(pc3 c u1 u2)→(pc3 c t1 t2)