DEFINITION lift_gen_lift()
TYPE =
       ∀t1:T
         .∀x:T
           .∀h1:nat
             .∀h2:nat
               .∀d1:nat
                 .∀d2:nat
                   .le d1 d2
                     →(eq T (lift h1 d1 t1) (lift h2 (plus d2 h1) x)
                          →ex2 T λt2:T.eq T x (lift h1 d1 t2) λt2:T.eq T t1 (lift h2 d2 t2))
BODY =
Show proof