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