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 =
Show proof