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