DEFINITION drop1_cons_tail()
TYPE =
       ∀c2:C
         .∀c3:C
           .∀h:nat
             .∀d:nat
               .(drop h d c2 c3)→∀hds:PList.∀c1:C.(drop1 hds c1 c2)→(drop1 (PConsTail hds h d) c1 c3)
BODY =
        assume c2: C
        assume c3: C
        assume h: nat
        assume d: nat
        suppose H: drop h d c2 c3
        assume hds: PList
          we proceed by induction on hds to prove ∀c1:C.(drop1 hds c1 c2)→(drop1 (PConsTail hds h d) c1 c3)
             case PNil : ⇒
                the thesis becomes ∀c1:C.(drop1 PNil c1 c2)→(drop1 (PConsTail PNil h d) c1 c3)
                    assume c1: C
                    suppose H0: drop1 PNil c1 c2
                      (H_y) 
                         by (drop1_gen_pnil . . H0)
eq C c1 c2
                      end of H_y
                      by (drop1_nil .)
                      we proved drop1 PNil c3 c3
                      by (drop1_cons . . . . H . . previous)
                      we proved drop1 (PCons h d PNil) c2 c3
                      by (eq_ind_r . . . previous . H_y)
                      we proved drop1 (PCons h d PNil) c1 c3
                      that is equivalent to drop1 (PConsTail PNil h d) c1 c3
∀c1:C.(drop1 PNil c1 c2)→(drop1 (PConsTail PNil h d) c1 c3)
             case PCons : n:nat n0:nat p:PList ⇒
                the thesis becomes ∀c1:C.∀H1:(drop1 (PCons n n0 p) c1 c2).(drop1 (PCons n n0 (PConsTail p h d)) c1 c3)
                (H0) by induction hypothesis we know ∀c1:C.(drop1 p c1 c2)→(drop1 (PConsTail p h d) c1 c3)
                    assume c1: C
                    suppose H1: drop1 (PCons n n0 p) c1 c2
                      (H_x) 
                         by (drop1_gen_pcons . . . . . H1)
ex2 C λc2:C.drop n n0 c1 c2 λc2:C.drop1 p c2 c2
                      end of H_x
                      (H2) consider H_x
                      we proceed by induction on H2 to prove drop1 (PCons n n0 (PConsTail p h d)) c1 c3
                         case ex_intro2 : x:C H3:drop n n0 c1 x H4:drop1 p x c2 ⇒
                            the thesis becomes drop1 (PCons n n0 (PConsTail p h d)) c1 c3
                               by (H0 . H4)
                               we proved drop1 (PConsTail p h d) x c3
                               by (drop1_cons . . . . H3 . . previous)
drop1 (PCons n n0 (PConsTail p h d)) c1 c3
                      we proved drop1 (PCons n n0 (PConsTail p h d)) c1 c3
                      that is equivalent to drop1 (PConsTail (PCons n n0 p) h d) c1 c3
∀c1:C.∀H1:(drop1 (PCons n n0 p) c1 c2).(drop1 (PCons n n0 (PConsTail p h d)) c1 c3)
          we proved ∀c1:C.(drop1 hds c1 c2)→(drop1 (PConsTail hds h d) c1 c3)
       we proved 
          ∀c2:C
            .∀c3:C
              .∀h:nat
                .∀d:nat
                  .(drop h d c2 c3)→∀hds:PList.∀c1:C.(drop1 hds c1 c2)→(drop1 (PConsTail hds h d) c1 c3)