DEFINITION arity_lift()
TYPE =
       ∀g:G
         .∀c2:C
           .∀t:T
             .∀a:A
               .arity g c2 t a
                 →∀c1:C.∀h:nat.∀d:nat.(drop h d c1 c2)→(arity g c1 (lift h d t) a)
BODY =
Show proof