DEFINITION arity_fsubst0()
TYPE =
       ∀g:G
         .∀c1:C
           .∀t1:T
             .∀a:A
               .arity g c1 t1 a
                 →∀d1:C
                      .∀u:T
                        .∀i:nat
                          .(getl i c1 (CHead d1 (Bind Abbr) u))→∀c2:C.∀t2:T.(fsubst0 i u c1 t1 c2 t2)→(arity g c2 t2 a)
BODY =
Show proof