DEFINITION subst0_lift_ge_s()
TYPE =
       ∀t1:T
         .∀t2:T
           .∀u:T
             .∀i:nat
               .subst0 i u t1 t2
                 →∀d:nat
                      .le d i
                        →∀b:B.(subst0 (s (Bind b) i) u (lift (S O) d t1) (lift (S O) d t2))
BODY =
        assume t1: T
        assume t2: T
        assume u: T
        assume i: nat
        suppose H: subst0 i u t1 t2
        assume d: nat
        suppose H0: le d i
        assume : B
          by (subst0_lift_ge_S . . . . H . H0)
          we proved subst0 (S i) u (lift (S O) d t1) (lift (S O) d t2)
          that is equivalent to subst0 (s (Bind __1) i) u (lift (S O) d t1) (lift (S O) d t2)
       we proved 
          ∀t1:T
            .∀t2:T
              .∀u:T
                .∀i:nat
                  .subst0 i u t1 t2
                    →∀d:nat
                         .le d i
                           →B→(subst0 (s (Bind __1) i) u (lift (S O) d t1) (lift (S O) d t2))