e)).(drop1_cons (CHead c (Bind b) (lift n n0 (lift1 p u))) (CHead x (Bind b)
(lift1 p u)) n (S n0) (drop_skip_bind n n0 c x H2 b (lift1 p u)) (CHead e
(Bind b) u) (Ss p) (H x u H3))))) H1)))))))))) hds))).
e)).(drop1_cons (CHead c (Bind b) (lift n n0 (lift1 p u))) (CHead x (Bind b)
(lift1 p u)) n (S n0) (drop_skip_bind n n0 c x H2 b (lift1 p u)) (CHead e
(Bind b) u) (Ss p) (H x u H3))))) H1)))))))))) hds))).