DEFINITION drop_ind()
TYPE =
       ∀P:nat→nat→C→C→Prop
         .∀c:C.(P O O c c)
           →(∀k:K
                  .∀n:nat
                    .∀c:C
                      .∀c1:C
                        .drop (r k n) O c c1
                          →(P (r k n) O c c1)→∀t:T.(P (S n) O (CHead c k t) c1)
                →(∀k:K
                       .∀n:nat
                         .∀n1:nat
                           .∀c:C
                             .∀c1:C
                               .drop n (r k n1) c c1
                                 →(P n (r k n1) c c1
                                      →∀t:T.(P n (S n1) (CHead c k (lift n (r k n1) t)) (CHead c1 k t)))
                     →∀n:nat.∀n1:nat.∀c:C.∀c1:C.(drop n n1 c c1)→(P n n1 c c1)))
BODY =
Show proof