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 =
Show proof