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 =
        assume P: nat→nat→C→C→Prop
        suppose H: ∀c:C.(P O O c c)
        suppose H1: 
           ∀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)
        suppose H2: 
           ∀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)))
          (aux) by well-founded reasoning we prove ∀n:nat.∀n1:nat.∀c:C.∀c1:C.(drop n n1 c c1)→(P n n1 c c1)
           assume n: nat
           assume n1: nat
           assume c: C
           assume c1: C
           suppose H3: drop n n1 c c1
             by cases on H3 we prove P n n1 c c1
                case drop_refl c2:C ⇒
                   the thesis becomes P O O c2 c2
                   by (H .)
P O O c2 c2
                case drop_drop k:K n2:nat c2:C c3:C H4:drop (r k n2) O c2 c3 t:T ⇒
                   the thesis becomes P (S n2) O (CHead c2 k t) c3
                   by (aux . . . . H4)
                   we proved P (r k n2) O c2 c3
                   by (H1 . . . . H4 previous .)
P (S n2) O (CHead c2 k t) c3
                case drop_skip k:K n2:nat n3:nat c2:C c3:C H4:drop n2 (r k n3) c2 c3 t:T ⇒
                   the thesis becomes P n2 (S n3) (CHead c2 k (lift n2 (r k n3) t)) (CHead c3 k t)
                   by (aux . . . . H4)
                   we proved P n2 (r k n3) c2 c3
                   by (H2 . . . . . H4 previous .)
P n2 (S n3) (CHead c2 k (lift n2 (r k n3) t)) (CHead c3 k t)
             we proved P n n1 c c1
∀n:nat.∀n1:nat.∀c:C.∀c1:C.(drop n n1 c c1)→(P n n1 c c1)
          done
          consider aux
          we proved ∀n:nat.∀n1:nat.∀c:C.∀c1:C.(drop n n1 c c1)→(P n n1 c c1)
       we proved 
          ∀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)))