DEFINITION ty3_gen_cast()
TYPE =
       ∀g:G
         .∀c:C
           .∀t1:T
             .∀t2:T
               .∀x:T
                 .ty3 g c (THead (Flat Cast) t2 t1) x
                   →ex3 T λt0:T.pc3 c (THead (Flat Cast) t0 t2) x λ:T.ty3 g c t1 t2 λt0:T.ty3 g c t2 t0
BODY =
Show proof