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 =
        assume h: nat
        assume d: nat
        assume c: C
        assume e: C
        suppose H: drop h d c e
        assume b: B
        assume u: T
          by (refl_equal . .)
          we proved eq nat d d
          that is equivalent to eq nat (r (Bind b) d) d
          we proceed by induction on the previous result to prove 
             drop
               h
               S d
               CHead c (Bind b) (lift h d u)
               CHead e (Bind b) u
             case refl_equal : ⇒
                the thesis becomes 
                drop
                  h
                  S d
                  CHead c (Bind b) (lift h (r (Bind b) d) u)
                  CHead e (Bind b) u
                   consider H
                   we proved drop h d c e
                   that is equivalent to drop h (r (Bind b) d) c e
                   by (drop_skip . . . . . previous .)

                      drop
                        h
                        S d
                        CHead c (Bind b) (lift h (r (Bind b) d) u)
                        CHead e (Bind b) u
          we proved 
             drop
               h
               S d
               CHead c (Bind b) (lift h d u)
               CHead e (Bind b) u
       we proved 
          ∀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