DEFINITION ty3_tred()
TYPE =
       ∀g:G.∀c:C.∀u:T.∀t1:T.(ty3 g c u t1)→∀t2:T.(pr3 c t1 t2)→(ty3 g c u t2)
BODY =
Show proof