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 =
        assume g: G
        assume c: C
        assume t: T
        assume v: T
        suppose H: ty3 g c t v
          by (ty3_correct . . . . H)
          we proved ex T λt:T.ty3 g c v t
          we proceed by induction on the previous result to prove ex T λu:T.ty3 g c (THead (Flat Cast) v t) u
             case ex_intro : x:T H0:ty3 g c v x ⇒
                the thesis becomes ex T λu:T.ty3 g c (THead (Flat Cast) v t) u
                   by (ty3_cast . . . . H . H0)
                   we proved ty3 g c (THead (Flat Cast) v t) (THead (Flat Cast) x v)
                   by (ex_intro . . . previous)
ex T λu:T.ty3 g c (THead (Flat Cast) v t) u
          we proved ex T λu:T.ty3 g c (THead (Flat Cast) v t) u
       we proved 
          ∀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)