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