DEFINITION arity_lift1()
TYPE =
       ∀g:G
         .∀a:A
           .∀c2:C
             .∀hds:PList.∀c1:C.∀t:T.(drop1 hds c1 c2)→(arity g c2 t a)→(arity g c1 (lift1 hds t) a)
BODY =
Show proof