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