DEFINITION arity_gen_abst()
TYPE =
       ∀g:G
         .∀c:C
           .∀u:T
             .∀t:T
               .∀a:A
                 .arity g c (THead (Bind Abst) u t) a
                   →(ex3_2
                        A
                        A
                        λa1:A.λa2:A.eq A a (AHead a1 a2)
                        λa1:A.λ:A.arity g c u (asucc g a1)
                        λ:A.λa2:A.arity g (CHead c (Bind Abst) u) t a2)
BODY =
Show proof