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