DEFINITION subst0_lift_ge_S()
TYPE =
       ∀t1:T
         .∀t2:T
           .∀u:T
             .∀i:nat
               .subst0 i u t1 t2
                 →∀d:nat.(le d i)→(subst0 (S 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
          (h1) 
             by (refl_equal . .)
             we proved eq nat (S i) (S i)
eq nat (plus (S O) i) (S i)
          end of h1
          (h2) 
             by (plus_sym . .)
eq nat (plus i (S O)) (plus (S O) i)
          end of h2
          by (eq_ind_r . . . h1 . h2)
          we proved eq nat (plus i (S O)) (S i)
          we proceed by induction on the previous result to prove subst0 (S i) u (lift (S O) d t1) (lift (S O) d t2)
             case refl_equal : ⇒
                the thesis becomes subst0 (plus i (S O)) u (lift (S O) d t1) (lift (S O) d t2)
                   by (subst0_lift_ge . . . . . H . H0)
subst0 (plus i (S O)) u (lift (S O) d t1) (lift (S O) d t2)
          we proved subst0 (S 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)→(subst0 (S i) u (lift (S O) d t1) (lift (S O) d t2))