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