DEFINITION ty3_typecheck()
TYPE =
       ∀g:G.∀c:C.∀t:T.∀v:T.(ty3 g c t v)→(ex T λu:T.ty3 g c (THead (Flat Cast) v t) u)
BODY =
Show proof