DEFINITION arity_gen_bind()
TYPE =
       ∀b:B
         .not (eq B b Abst)
           →∀g:G
                .∀c:C
                  .∀u:T
                    .∀t:T
                      .∀a2:A
                        .arity g c (THead (Bind b) u t) a2
                          →ex2 A λa1:A.arity g c u a1 λ:A.arity g (CHead c (Bind b) u) t a2
BODY =
Show proof