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