DEFINITION subst0_ind()
TYPE =
       ∀P:nat→T→T→T→Prop
         .∀t:T.∀n:nat.(P n t (TLRef n) (lift (S n) O t))
           →(∀t:T
                  .∀t1:T.∀t2:T.∀n:nat.(subst0 n t t2 t1)→(P n t t2 t1)→∀t3:T.∀k:K.(P n t (THead k t2 t3) (THead k t1 t3))
                →(∀k:K
                       .∀t:T
                         .∀t1:T
                           .∀t2:T
                             .∀n:nat
                               .subst0 (s k n) t t2 t1
                                 →(P (s k n) t t2 t1)→∀t3:T.(P n t (THead k t3 t2) (THead k t3 t1))
                     →(∀t:T
                            .∀t1:T
                              .∀t2:T
                                .∀n:nat
                                  .subst0 n t t1 t2
                                    →(P n t t1 t2
                                         →∀k:K
                                              .∀t3:T
                                                .∀t4:T
                                                  .(subst0 (s k n) t t3 t4)→(P (s k n) t t3 t4)→(P n t (THead k t1 t3) (THead k t2 t4)))
                          →∀n:nat.∀t:T.∀t1:T.∀t2:T.(subst0 n t t1 t2)→(P n t t1 t2))))
BODY =
        assume P: nat→T→T→T→Prop
        suppose H: ∀t:T.∀n:nat.(P n t (TLRef n) (lift (S n) O t))
        suppose H1: 
           ∀t:T
             .∀t1:T.∀t2:T.∀n:nat.(subst0 n t t2 t1)→(P n t t2 t1)→∀t3:T.∀k:K.(P n t (THead k t2 t3) (THead k t1 t3))
        suppose H2: 
           ∀k:K
             .∀t:T
               .∀t1:T
                 .∀t2:T
                   .∀n:nat
                     .subst0 (s k n) t t2 t1
                       →(P (s k n) t t2 t1)→∀t3:T.(P n t (THead k t3 t2) (THead k t3 t1))
        suppose H3: 
           ∀t:T
             .∀t1:T
               .∀t2:T
                 .∀n:nat
                   .subst0 n t t1 t2
                     →(P n t t1 t2
                          →∀k:K
                               .∀t3:T
                                 .∀t4:T
                                   .(subst0 (s k n) t t3 t4)→(P (s k n) t t3 t4)→(P n t (THead k t1 t3) (THead k t2 t4)))
          (aux) by well-founded reasoning we prove ∀n:nat.∀t:T.∀t1:T.∀t2:T.(subst0 n t t1 t2)→(P n t t1 t2)
           assume n: nat
           assume t: T
           assume t1: T
           assume t2: T
           suppose H4: subst0 n t t1 t2
             by cases on H4 we prove P n t t1 t2
                case subst0_lref t3:T n1:nat ⇒
                   the thesis becomes P n1 t3 (TLRef n1) (lift (S n1) O t3)
                   by (H . .)
P n1 t3 (TLRef n1) (lift (S n1) O t3)
                case subst0_fst t3:T t4:T t5:T n1:nat H5:subst0 n1 t3 t5 t4 t6:T k:K ⇒
                   the thesis becomes P n1 t3 (THead k t5 t6) (THead k t4 t6)
                   by (aux . . . . H5)
                   we proved P n1 t3 t5 t4
                   by (H1 . . . . H5 previous . .)
P n1 t3 (THead k t5 t6) (THead k t4 t6)
                case subst0_snd k:K t3:T t4:T t5:T n1:nat H5:subst0 (s k n1) t3 t5 t4 t6:T ⇒
                   the thesis becomes P n1 t3 (THead k t6 t5) (THead k t6 t4)
                   by (aux . . . . H5)
                   we proved P (s k n1) t3 t5 t4
                   by (H2 . . . . . H5 previous .)
P n1 t3 (THead k t6 t5) (THead k t6 t4)
                case subst0_both t3:T t4:T t5:T n1:nat H5:subst0 n1 t3 t4 t5 k:K t6:T t7:T H6:subst0 (s k n1) t3 t6 t7 ⇒
                   the thesis becomes P n1 t3 (THead k t4 t6) (THead k t5 t7)
                   (h1) by (aux . . . . H5) we proved P n1 t3 t4 t5
                   (h2) 
                      by (aux . . . . H6)
P (s k n1) t3 t6 t7
                   end of h2
                   by (H3 . . . . H5 h1 . . . H6 h2)
P n1 t3 (THead k t4 t6) (THead k t5 t7)
             we proved P n t t1 t2
∀n:nat.∀t:T.∀t1:T.∀t2:T.(subst0 n t t1 t2)→(P n t t1 t2)
          done
          consider aux
          we proved ∀n:nat.∀t:T.∀t1:T.∀t2:T.(subst0 n t t1 t2)→(P n t t1 t2)
       we proved 
          ∀P:nat→T→T→T→Prop
            .∀t:T.∀n:nat.(P n t (TLRef n) (lift (S n) O t))
              →(∀t:T
                     .∀t1:T.∀t2:T.∀n:nat.(subst0 n t t2 t1)→(P n t t2 t1)→∀t3:T.∀k:K.(P n t (THead k t2 t3) (THead k t1 t3))
                   →(∀k:K
                          .∀t:T
                            .∀t1:T
                              .∀t2:T
                                .∀n:nat
                                  .subst0 (s k n) t t2 t1
                                    →(P (s k n) t t2 t1)→∀t3:T.(P n t (THead k t3 t2) (THead k t3 t1))
                        →(∀t:T
                               .∀t1:T
                                 .∀t2:T
                                   .∀n:nat
                                     .subst0 n t t1 t2
                                       →(P n t t1 t2
                                            →∀k:K
                                                 .∀t3:T
                                                   .∀t4:T
                                                     .(subst0 (s k n) t t3 t4)→(P (s k n) t t3 t4)→(P n t (THead k t1 t3) (THead k t2 t4)))
                             →∀n:nat.∀t:T.∀t1:T.∀t2:T.(subst0 n t t1 t2)→(P n t t1 t2))))