DEFINITION subst1_gen_lift_ge()
TYPE =
       ∀u:T
         .∀t1:T
           .∀x:T
             .∀i:nat
               .∀h:nat
                 .∀d:nat
                   .subst1 i u (lift h d t1) x
                     →(le (plus d h) i
                          →ex2 T λt2:T.eq T x (lift h d t2) λt2:T.subst1 (minus i h) u t1 t2)
BODY =
Show proof