DEFINITION sn3_appls_cast()
TYPE =
       ∀c:C
         .∀vs:TList
           .∀u:T
             .sn3 c (THeads (Flat Appl) vs u)
               →∀t:T
                    .sn3 c (THeads (Flat Appl) vs t)
                      →sn3 c (THeads (Flat Appl) vs (THead (Flat Cast) u t))
BODY =
Show proof