DEFINITION wf3_ty3()
TYPE =
       ∀g:G.∀c1:C.∀t:T.∀u:T.(ty3 g c1 t u)→(ex2 C λc2:C.wf3 g c1 c2 λc2:C.ty3 g c2 t u)
BODY =
        assume g: G
        assume c1: C
        assume t: T
        assume u: T
        suppose H: ty3 g c1 t u
          (H_x) 
             by (wf3_total . .)
ex C λc2:C.wf3 g c1 c2
          end of H_x
          (H0) consider H_x
          we proceed by induction on H0 to prove ex2 C λc2:C.wf3 g c1 c2 λc2:C.ty3 g c2 t u
             case ex_intro : x:C H1:wf3 g c1 x ⇒
                the thesis becomes ex2 C λc2:C.wf3 g c1 c2 λc2:C.ty3 g c2 t u
                   by (wf3_ty3_conf . . . . H . H1)
                   we proved ty3 g x t u
                   by (ex_intro2 . . . . H1 previous)
ex2 C λc2:C.wf3 g c1 c2 λc2:C.ty3 g c2 t u
          we proved ex2 C λc2:C.wf3 g c1 c2 λc2:C.ty3 g c2 t u
       we proved ∀g:G.∀c1:C.∀t:T.∀u:T.(ty3 g c1 t u)→(ex2 C λc2:C.wf3 g c1 c2 λc2:C.ty3 g c2 t u)