DEFINITION drop_skip_bind()
TYPE =
       ∀h:nat
         .∀d:nat
           .∀c:C
             .∀e:C
               .drop h d c e
                 →∀b:B
                      .∀u:T
                        .drop
                          h
                          S d
                          CHead c (Bind b) (lift h d u)
                          CHead e (Bind b) u
BODY =
Show proof