DEFINITION sty0_gen_cast()
TYPE =
       ∀g:G
         .∀c:C
           .∀v1:T
             .∀t1:T
               .∀x:T
                 .sty0 g c (THead (Flat Cast) v1 t1) x
                   →ex3_2 T T λv2:T.λ:T.sty0 g c v1 v2 λ:T.λt2:T.sty0 g c t1 t2 λv2:T.λt2:T.eq T x (THead (Flat Cast) v2 t2)
BODY =
Show proof