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