DEFINITION subst1_lift_ge()
TYPE =
       ∀t1:T
         .∀t2:T
           .∀u:T
             .∀i:nat
               .∀h:nat
                 .subst1 i u t1 t2
                   →∀d:nat.(le d i)→(subst1 (plus i h) u (lift h d t1) (lift h d t2))
BODY =
Show proof