DEFINITION arity_subst0()
TYPE =
       ∀g:G
         .∀c:C
           .∀t1:T
             .∀a:A
               .arity g c t1 a
                 →∀d:C
                      .∀u:T
                        .∀i:nat
                          .getl i c (CHead d (Bind Abbr) u)
                            →∀t2:T.(subst0 i u t1 t2)→(arity g c t2 a)
BODY =
Show proof