DEFINITION ty3_sconv()
TYPE =
       ∀g:G.∀c:C.∀u1:T.∀t1:T.(ty3 g c u1 t1)→∀u2:T.∀t2:T.(ty3 g c u2 t2)→(pc3 c u1 u2)→(ty3 g c u1 t2)
BODY =
Show proof