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