DEFINITION pr2_gen_lift()
TYPE =
       ∀c:C
         .∀t1:T
           .∀x:T
             .∀h:nat
               .∀d:nat
                 .pr2 c (lift h d t1) x
                   →∀e:C.(drop h d c e)→(ex2 T λt2:T.eq T x (lift h d t2) λt2:T.pr2 e t1 t2)
BODY =
Show proof