DEFINITION arity_gen_appl()
TYPE =
       ∀g:G
         .∀c:C
           .∀u:T
             .∀t:T
               .∀a2:A
                 .arity g c (THead (Flat Appl) u t) a2
                   →ex2 A λa1:A.arity g c u a1 λa1:A.arity g c t (AHead a1 a2)
BODY =
Show proof