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 =
        assume c: C
        assume e: C
        assume h: nat
        assume d: nat
        suppose H: drop h d c e
        assume t1: T
        assume t2: T
        suppose H0: pc3 e t1 t2
          (H1) consider H0
          consider H1
          we proved pc3 e t1 t2
          that is equivalent to ex2 T λt:T.pr3 e t1 t λt:T.pr3 e t2 t
          we proceed by induction on the previous result to prove pc3 c (lift h d t1) (lift h d t2)
             case ex_intro2 : x:T H2:pr3 e t1 x H3:pr3 e t2 x ⇒
                the thesis becomes pc3 c (lift h d t1) (lift h d t2)
                   (h1) 
                      by (pr3_lift . . . . H . . H2)
pr3 c (lift h d t1) (lift h d x)
                   end of h1
                   (h2) 
                      by (pr3_lift . . . . H . . H3)
pr3 c (lift h d t2) (lift h d x)
                   end of h2
                   by (pc3_pr3_t . . . h1 . h2)
pc3 c (lift h d t1) (lift h d t2)
          we proved pc3 c (lift h d t1) (lift h d t2)
       we proved 
          ∀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))