DEFINITION arity_gen_appls()
TYPE =
       ∀g:G
         .∀c:C
           .∀t:T
             .∀vs:TList
               .∀a2:A
                 .arity g c (THeads (Flat Appl) vs t) a2
                   →ex A λa:A.arity g c t a
BODY =
Show proof