DEFINITION arity_appls_abbr()
TYPE =
       ∀g:G
         .∀c:C
           .∀d:C
             .∀v:T
               .∀i:nat
                 .getl i c (CHead d (Bind Abbr) v)
                   →∀vs:TList
                        .∀a:A
                          .arity g c (THeads (Flat Appl) vs (lift (S i) O v)) a
                            →arity g c (THeads (Flat Appl) vs (TLRef i)) a
BODY =
Show proof