DEFINITION sc3_cast()
TYPE =
       g:G
         .a:A
           .vs:TList
             .c:C
               .u:T
                 .sc3 g (asucc g a) c (THeads (Flat Appl) vs u)
                   t:T
                        .sc3 g a c (THeads (Flat Appl) vs t)
                          sc3 g a c (THeads (Flat Appl) vs (THead (Flat Cast) u t))
BODY =
Show proof