DEFINITION arity_appls_bind()
TYPE =
       ∀g:G
         .∀b:B
           .not (eq B b Abst)
             →∀c:C
                  .∀v:T
                    .∀a1:A
                      .arity g c v a1
                        →∀t:T
                             .∀vs:TList
                               .∀a2:A
                                 .(arity
                                     g
                                     CHead c (Bind b) v
                                     THeads (Flat Appl) (lifts (S O) O vs) t
                                     a2)
                                   →arity g c (THeads (Flat Appl) vs (THead (Bind b) v t)) a2
BODY =
Show proof