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