DEFINITION subst0_gen_lift_lt()
TYPE =
       ∀u:T
         .∀t1:T
           .∀x:T
             .∀i:nat
               .∀h:nat
                 .∀d:nat
                   .subst0 i (lift h d u) (lift h (S (plus i d)) t1) x
                     →ex2 T λt2:T.eq T x (lift h (S (plus i d)) t2) λt2:T.subst0 i u t1 t2
BODY =
Show proof