DEFINITION drop1_ind()
TYPE =
       ∀P:PList→C→C→Prop
         .∀c:C.(P PNil c c)
           →(∀c:C
                  .∀c1:C
                    .∀n:nat
                      .∀n1:nat
                        .(drop n n1 c c1)→∀c2:C.∀p:PList.(drop1 p c1 c2)→(P p c1 c2)→(P (PCons n n1 p) c c2)
                →∀p:PList.∀c:C.∀c1:C.(drop1 p c c1)→(P p c c1))
BODY =
        assume P: PList→C→C→Prop
        suppose H: ∀c:C.(P PNil c c)
        suppose H1: 
           ∀c:C
             .∀c1:C
               .∀n:nat
                 .∀n1:nat
                   .(drop n n1 c c1)→∀c2:C.∀p:PList.(drop1 p c1 c2)→(P p c1 c2)→(P (PCons n n1 p) c c2)
          (aux) by well-founded reasoning we prove ∀p:PList.∀c:C.∀c1:C.(drop1 p c c1)→(P p c c1)
           assume p: PList
           assume c: C
           assume c1: C
           suppose H2: drop1 p c c1
             by cases on H2 we prove P p c c1
                case drop1_nil c2:C ⇒
                   the thesis becomes P PNil c2 c2
                   by (H .)
P PNil c2 c2
                case drop1_cons c2:C c3:C n:nat n1:nat H3:drop n n1 c2 c3 c4:C p1:PList H4:drop1 p1 c3 c4 ⇒
                   the thesis becomes P (PCons n n1 p1) c2 c4
                   by (aux . . . H4)
                   we proved P p1 c3 c4
                   by (H1 . . . . H3 . . H4 previous)
P (PCons n n1 p1) c2 c4
             we proved P p c c1
∀p:PList.∀c:C.∀c1:C.(drop1 p c c1)→(P p c c1)
          done
          consider aux
          we proved ∀p:PList.∀c:C.∀c1:C.(drop1 p c c1)→(P p c c1)
       we proved 
          ∀P:PList→C→C→Prop
            .∀c:C.(P PNil c c)
              →(∀c:C
                     .∀c1:C
                       .∀n:nat
                         .∀n1:nat
                           .(drop n n1 c c1)→∀c2:C.∀p:PList.(drop1 p c1 c2)→(P p c1 c2)→(P (PCons n n1 p) c c2)
                   →∀p:PList.∀c:C.∀c1:C.(drop1 p c c1)→(P p c c1))