DEFINITION pr3_gen_lift()
TYPE =
       ∀c:C
         .∀t1:T
           .∀x:T
             .∀h:nat
               .∀d:nat
                 .pr3 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.pr3 e t1 t2)
BODY =
Show proof