(H: (drop h d c e)).(\lambda (b: B).(\lambda (u: T).(eq_ind nat (r (Bind b)
d) (\lambda (n: nat).(drop h (S d) (CHead c (Bind b) (lift h n u)) (CHead e
(Bind b) u))) (drop_skip (Bind b) h d c e H u) d (refl_equal nat d)))))))).
(H: (drop h d c e)).(\lambda (b: B).(\lambda (u: T).(eq_ind nat (r (Bind b)
d) (\lambda (n: nat).(drop h (S d) (CHead c (Bind b) (lift h n u)) (CHead e
(Bind b) u))) (drop_skip (Bind b) h d c e H u) d (refl_equal nat d)))))))).