DEFINITION subst1_ind()
TYPE =
       ∀i:nat
         .∀v:T
           .∀t1:T
             .∀P:T→Prop
               .(P t1)→(∀t:T.(subst0 i v t1 t)→(P t))→∀t:T.(subst1 i v t1 t)→(P t)
BODY =
        assume i: nat
        assume v: T
        assume t1: T
        assume P: T→Prop
        suppose H: P t1
        suppose H1: ∀t:T.(subst0 i v t1 t)→(P t)
        assume t: T
        suppose H2: subst1 i v t1 t
          by cases on H2 we prove P t
             case subst1_refl ⇒
                the thesis becomes the hypothesis H
             case subst1_single t2:T H3:subst0 i v t1 t2 ⇒
                the thesis becomes P t2
                by (H1 . H3)
P t2
          we proved P t
       we proved 
          ∀i:nat
            .∀v:T
              .∀t1:T
                .∀P:T→Prop
                  .(P t1)→(∀t:T.(subst0 i v t1 t)→(P t))→∀t:T.(subst1 i v t1 t)→(P t)