DEFINITION drop1_skip_bind()
TYPE =
       ∀b:B
         .∀e:C
           .∀hds:PList
             .∀c:C
               .∀u:T
                 .drop1 hds c e
                   →drop1 (Ss hds) (CHead c (Bind b) (lift1 hds u)) (CHead e (Bind b) u)
BODY =
        assume b: B
        assume e: C
        assume hds: PList
          we proceed by induction on hds to prove 
             ∀c:C
               .∀u:T
                 .drop1 hds c e
                   →drop1 (Ss hds) (CHead c (Bind b) (lift1 hds u)) (CHead e (Bind b) u)
             case PNil : ⇒
                the thesis becomes 
                ∀c:C
                  .∀u:T
                    .drop1 PNil c e
                      →drop1 (Ss PNil) (CHead c (Bind b) (lift1 PNil u)) (CHead e (Bind b) u)
                    assume c: C
                    assume u: T
                    suppose H: drop1 PNil c e
                      (H_y) 
                         by (drop1_gen_pnil . . H)
eq C c e
                      end of H_y
                      by (drop1_nil .)
                      we proved drop1 PNil (CHead e (Bind b) u) (CHead e (Bind b) u)
                      by (eq_ind_r . . . previous . H_y)
                      we proved drop1 PNil (CHead c (Bind b) u) (CHead e (Bind b) u)
                      that is equivalent to 
                         drop1 (Ss PNil) (CHead c (Bind b) (lift1 PNil u)) (CHead e (Bind b) u)

                      ∀c:C
                        .∀u:T
                          .drop1 PNil c e
                            →drop1 (Ss PNil) (CHead c (Bind b) (lift1 PNil u)) (CHead e (Bind b) u)
             case PCons : n:nat n0:nat p:PList ⇒
                the thesis becomes 
                ∀c:C
                  .∀u:T
                    .∀H0:drop1 (PCons n n0 p) c e
                      .drop1
                        PCons n (S n0) (Ss p)
                        CHead c (Bind b) (lift n n0 (lift1 p u))
                        CHead e (Bind b) u
                (H) by induction hypothesis we know 
                   ∀c:C
                     .∀u:T
                       .drop1 p c e
                         →drop1 (Ss p) (CHead c (Bind b) (lift1 p u)) (CHead e (Bind b) u)
                    assume c: C
                    assume u: T
                    suppose H0: drop1 (PCons n n0 p) c e
                      (H_x) 
                         by (drop1_gen_pcons . . . . . H0)
ex2 C λc2:C.drop n n0 c c2 λc2:C.drop1 p c2 e
                      end of H_x
                      (H1) consider H_x
                      we proceed by induction on H1 to prove 
                         drop1
                           PCons n (S n0) (Ss p)
                           CHead c (Bind b) (lift n n0 (lift1 p u))
                           CHead e (Bind b) u
                         case ex_intro2 : x:C H2:drop n n0 c x H3:drop1 p x e ⇒
                            the thesis becomes 
                            drop1
                              PCons n (S n0) (Ss p)
                              CHead c (Bind b) (lift n n0 (lift1 p u))
                              CHead e (Bind b) u
                               (h1) 
                                  by (drop_skip_bind . . . . H2 . .)

                                     drop
                                       n
                                       S n0
                                       CHead c (Bind b) (lift n n0 (lift1 p u))
                                       CHead x (Bind b) (lift1 p u)
                               end of h1
                               (h2) 
                                  by (H . . H3)
drop1 (Ss p) (CHead x (Bind b) (lift1 p u)) (CHead e (Bind b) u)
                               end of h2
                               by (drop1_cons . . . . h1 . . h2)

                                  drop1
                                    PCons n (S n0) (Ss p)
                                    CHead c (Bind b) (lift n n0 (lift1 p u))
                                    CHead e (Bind b) u
                      we proved 
                         drop1
                           PCons n (S n0) (Ss p)
                           CHead c (Bind b) (lift n n0 (lift1 p u))
                           CHead e (Bind b) u
                      that is equivalent to 
                         drop1
                           Ss (PCons n n0 p)
                           CHead c (Bind b) (lift1 (PCons n n0 p) u)
                           CHead e (Bind b) u

                      ∀c:C
                        .∀u:T
                          .∀H0:drop1 (PCons n n0 p) c e
                            .drop1
                              PCons n (S n0) (Ss p)
                              CHead c (Bind b) (lift n n0 (lift1 p u))
                              CHead e (Bind b) u
          we proved 
             ∀c:C
               .∀u:T
                 .drop1 hds c e
                   →drop1 (Ss hds) (CHead c (Bind b) (lift1 hds u)) (CHead e (Bind b) u)
       we proved 
          ∀b:B
            .∀e:C
              .∀hds:PList
                .∀c:C
                  .∀u:T
                    .drop1 hds c e
                      →drop1 (Ss hds) (CHead c (Bind b) (lift1 hds u)) (CHead e (Bind b) u)