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