DEFINITION wf3_pc3_conf()
TYPE =
       ∀g:G.∀c1:C.∀t1:T.∀t2:T.(pc3 c1 t1 t2)→∀c2:C.(wf3 g c1 c2)→∀u1:T.(ty3 g c1 t1 u1)→∀u2:T.(ty3 g c1 t2 u2)→(pc3 c2 t1 t2)
BODY =
        assume g: G
        assume c1: C
        assume t1: T
        assume t2: T
        suppose H: pc3 c1 t1 t2
        assume c2: C
        suppose H0: wf3 g c1 c2
        assume u1: T
        suppose H1: ty3 g c1 t1 u1
        assume u2: T
        suppose H2: ty3 g c1 t2 u2
          (H3) consider H
          consider H3
          we proved pc3 c1 t1 t2
          that is equivalent to ex2 T λt:T.pr3 c1 t1 t λt:T.pr3 c1 t2 t
          we proceed by induction on the previous result to prove pc3 c2 t1 t2
             case ex_intro2 : x:T H4:pr3 c1 t1 x H5:pr3 c1 t2 x ⇒
                the thesis becomes pc3 c2 t1 t2
                   (h1) 
                      by (wf3_pr3_conf . . . . H4 . H0 . H1)
pr3 c2 t1 x
                   end of h1
                   (h2) 
                      by (wf3_pr3_conf . . . . H5 . H0 . H2)
pr3 c2 t2 x
                   end of h2
                   by (pc3_pr3_t . . . h1 . h2)
pc3 c2 t1 t2
          we proved pc3 c2 t1 t2
       we proved ∀g:G.∀c1:C.∀t1:T.∀t2:T.(pc3 c1 t1 t2)→∀c2:C.(wf3 g c1 c2)→∀u1:T.(ty3 g c1 t1 u1)→∀u2:T.(ty3 g c1 t2 u2)→(pc3 c2 t1 t2)