DEFINITION drop_skip_flat()
TYPE =
       ∀h:nat
         .∀d:nat
           .∀c:C
             .∀e:C
               .drop h (S d) c e
                 →∀f:F
                      .∀u:T
                        .drop
                          h
                          S d
                          CHead c (Flat f) (lift h (S d) u)
                          CHead e (Flat f) u
BODY =
        assume h: nat
        assume d: nat
        assume c: C
        assume e: C
        suppose H: drop h (S d) c e
        assume f: F
        assume u: T
          by (refl_equal . .)
          we proved eq nat (S d) (S d)
          that is equivalent to eq nat (r (Flat f) d) (S d)
          we proceed by induction on the previous result to prove 
             drop
               h
               S d
               CHead c (Flat f) (lift h (S d) u)
               CHead e (Flat f) u
             case refl_equal : ⇒
                the thesis becomes 
                drop
                  h
                  S d
                  CHead c (Flat f) (lift h (r (Flat f) d) u)
                  CHead e (Flat f) u
                   consider H
                   we proved drop h (S d) c e
                   that is equivalent to drop h (r (Flat f) d) c e
                   by (drop_skip . . . . . previous .)

                      drop
                        h
                        S d
                        CHead c (Flat f) (lift h (r (Flat f) d) u)
                        CHead e (Flat f) u
          we proved 
             drop
               h
               S d
               CHead c (Flat f) (lift h (S d) u)
               CHead e (Flat f) u
       we proved 
          ∀h:nat
            .∀d:nat
              .∀c:C
                .∀e:C
                  .drop h (S d) c e
                    →∀f:F
                         .∀u:T
                           .drop
                             h
                             S d
                             CHead c (Flat f) (lift h (S d) u)
                             CHead e (Flat f) u