DEFINITION pr3_lift()
TYPE =
       ∀c:C
         .∀e:C
           .∀h:nat
             .∀d:nat.(drop h d c e)→∀t1:T.∀t2:T.(pr3 e t1 t2)→(pr3 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: pr3 e t1 t2
          we proceed by induction on H0 to prove pr3 c (lift h d t1) (lift h d t2)
             case pr3_refl : t:T ⇒
                the thesis becomes pr3 c (lift h d t) (lift h d t)
                   by (pr3_refl . .)
pr3 c (lift h d t) (lift h d t)
             case pr3_sing : t0:T t3:T H1:pr2 e t3 t0 t4:T :pr3 e t0 t4 ⇒
                the thesis becomes pr3 c (lift h d t3) (lift h d t4)
                (H3) by induction hypothesis we know pr3 c (lift h d t0) (lift h d t4)
                   by (pr2_lift . . . . H . . H1)
                   we proved pr2 c (lift h d t3) (lift h d t0)
                   by (pr3_sing . . . previous . H3)
pr3 c (lift h d t3) (lift h d t4)
          we proved pr3 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.(pr3 e t1 t2)→(pr3 c (lift h d t1) (lift h d t2))