DEFINITION csubst0_ind()
TYPE =
       ∀P:nat→T→C→C→Prop
         .∀k:K.∀n:nat.∀t:T.∀t1:T.∀t2:T.(subst0 n t t1 t2)→∀c:C.(P (s k n) t (CHead c k t1) (CHead c k t2))
           →(∀k:K
                  .∀n:nat
                    .∀c:C
                      .∀c1:C
                        .∀t:T
                          .(csubst0 n t c c1)→(P n t c c1)→∀t1:T.(P (s k n) t (CHead c k t1) (CHead c1 k t1))
                →(∀k:K
                       .∀n:nat
                         .∀t:T
                           .∀t1:T
                             .∀t2:T
                               .subst0 n t t1 t2
                                 →∀c:C
                                      .∀c1:C.(csubst0 n t c c1)→(P n t c c1)→(P (s k n) t (CHead c k t1) (CHead c1 k t2))
                     →∀n:nat.∀t:T.∀c:C.∀c1:C.(csubst0 n t c c1)→(P n t c c1)))
BODY =
        assume P: nat→T→C→C→Prop
        suppose H: ∀k:K.∀n:nat.∀t:T.∀t1:T.∀t2:T.(subst0 n t t1 t2)→∀c:C.(P (s k n) t (CHead c k t1) (CHead c k t2))
        suppose H1: 
           ∀k:K
             .∀n:nat
               .∀c:C
                 .∀c1:C
                   .∀t:T
                     .(csubst0 n t c c1)→(P n t c c1)→∀t1:T.(P (s k n) t (CHead c k t1) (CHead c1 k t1))
        suppose H2: 
           ∀k:K
             .∀n:nat
               .∀t:T
                 .∀t1:T
                   .∀t2:T
                     .subst0 n t t1 t2
                       →∀c:C
                            .∀c1:C.(csubst0 n t c c1)→(P n t c c1)→(P (s k n) t (CHead c k t1) (CHead c1 k t2))
          (aux) by well-founded reasoning we prove ∀n:nat.∀t:T.∀c:C.∀c1:C.(csubst0 n t c c1)→(P n t c c1)
           assume n: nat
           assume t: T
           assume c: C
           assume c1: C
           suppose H3: csubst0 n t c c1
             by cases on H3 we prove P n t c c1
                case csubst0_snd k:K n1:nat t1:T t2:T t3:T H4:subst0 n1 t1 t2 t3 c2:C ⇒
                   the thesis becomes P (s k n1) t1 (CHead c2 k t2) (CHead c2 k t3)
                   by (H . . . . . H4 .)
P (s k n1) t1 (CHead c2 k t2) (CHead c2 k t3)
                case csubst0_fst k:K n1:nat c2:C c3:C t1:T H4:csubst0 n1 t1 c2 c3 t2:T ⇒
                   the thesis becomes P (s k n1) t1 (CHead c2 k t2) (CHead c3 k t2)
                   by (aux . . . . H4)
                   we proved P n1 t1 c2 c3
                   by (H1 . . . . . H4 previous .)
P (s k n1) t1 (CHead c2 k t2) (CHead c3 k t2)
                case csubst0_both k:K n1:nat t1:T t2:T t3:T H4:subst0 n1 t1 t2 t3 c2:C c3:C H5:csubst0 n1 t1 c2 c3 ⇒
                   the thesis becomes P (s k n1) t1 (CHead c2 k t2) (CHead c3 k t3)
                   by (aux . . . . H5)
                   we proved P n1 t1 c2 c3
                   by (H2 . . . . . H4 . . H5 previous)
P (s k n1) t1 (CHead c2 k t2) (CHead c3 k t3)
             we proved P n t c c1
∀n:nat.∀t:T.∀c:C.∀c1:C.(csubst0 n t c c1)→(P n t c c1)
          done
          consider aux
          we proved ∀n:nat.∀t:T.∀c:C.∀c1:C.(csubst0 n t c c1)→(P n t c c1)
       we proved 
          ∀P:nat→T→C→C→Prop
            .∀k:K.∀n:nat.∀t:T.∀t1:T.∀t2:T.(subst0 n t t1 t2)→∀c:C.(P (s k n) t (CHead c k t1) (CHead c k t2))
              →(∀k:K
                     .∀n:nat
                       .∀c:C
                         .∀c1:C
                           .∀t:T
                             .(csubst0 n t c c1)→(P n t c c1)→∀t1:T.(P (s k n) t (CHead c k t1) (CHead c1 k t1))
                   →(∀k:K
                          .∀n:nat
                            .∀t:T
                              .∀t1:T
                                .∀t2:T
                                  .subst0 n t t1 t2
                                    →∀c:C
                                         .∀c1:C.(csubst0 n t c c1)→(P n t c c1)→(P (s k n) t (CHead c k t1) (CHead c1 k t2))
                        →∀n:nat.∀t:T.∀c:C.∀c1:C.(csubst0 n t c c1)→(P n t c c1)))