(lift n n0 (lift1 p t)) a) (\lambda (x: C).(\lambda (H3: (drop n n0 c1
x)).(\lambda (H4: (drop1 p x c2)).(arity_lift g x (lift1 p t) a (H x t H4 H1)
c1 n n0 H3)))) H2))))))))))) hds)))).
(lift n n0 (lift1 p t)) a) (\lambda (x: C).(\lambda (H3: (drop n n0 c1
x)).(\lambda (H4: (drop1 p x c2)).(arity_lift g x (lift1 p t) a (H x t H4 H1)
c1 n n0 H3)))) H2))))))))))) hds)))).