DEFINITION arity_appls_appl()
TYPE =
       ∀g:G
         .∀c:C
           .∀v:T
             .∀a1:A
               .arity g c v a1
                 →∀u:T
                      .arity g c u (asucc g a1)
                        →∀t:T
                             .∀vs:TList
                               .∀a2:A
                                 .arity g c (THeads (Flat Appl) vs (THead (Bind Abbr) v t)) a2
                                   →(arity
                                        g
                                        c
                                        THeads
                                          Flat Appl
                                          vs
                                          THead (Flat Appl) v (THead (Bind Abst) u t)
                                        a2)
BODY =
Show proof