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