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 =
        assume g: G
        assume c: C
        assume t1: T
        assume a: A
        suppose H: arity g c t1 a
        assume d: C
        assume u: T
        assume i: nat
        suppose H0: getl i c (CHead d (Bind Abbr) u)
        assume t2: T
        suppose H1: subst0 i u t1 t2
          by (fsubst0_snd . . . . . H1)
          we proved fsubst0 i u c t1 c t2
          by (arity_fsubst0 . . . . H . . . H0 . . previous)
          we proved arity g c t2 a
       we proved 
          ∀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)