DEFINITION arity_aprem()
TYPE =
       ∀g:G
         .∀c:C
           .∀t:T
             .∀a:A
               .arity g c t a
                 →∀i:nat
                      .∀b:A
                        .aprem i a b
                          →(ex2_3
                               C
                               T
                               nat
                               λd:C.λ:T.λj:nat.drop (plus i j) O d c
                               λd:C.λu:T.λ:nat.arity g d u (asucc g b))
BODY =
Show proof