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