DEFINITION sty1_cast2()
TYPE =
       ∀g:G
         .∀c:C
           .∀t1:T
             .∀t2:T
               .sty1 g c t1 t2
                 →∀v1:T
                      .∀v2:T
                        .sty0 g c v1 v2
                          →ex2 T λv3:T.sty1 g c v1 v3 λv3:T.sty1 g c (THead (Flat Cast) v1 t1) (THead (Flat Cast) v3 t2)
BODY =
Show proof