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 =
        assume c: C
        assume t1: T
        assume t2: T
        assume h: nat
        assume d: nat
        suppose H: pc3 c (lift h d t1) (lift h d t2)
        assume e: C
        suppose H0: drop h d c e
          (H1) consider H
          consider H1
          we proved pc3 c (lift h d t1) (lift h d t2)
          that is equivalent to ex2 T λt:T.pr3 c (lift h d t1) t λt:T.pr3 c (lift h d t2) t
          we proceed by induction on the previous result to prove pc3 e t1 t2
             case ex_intro2 : x:T H2:pr3 c (lift h d t1) x H3:pr3 c (lift h d t2) x ⇒
                the thesis becomes pc3 e t1 t2
                   (H4) 
                      by (pr3_gen_lift . . . . . H3 . H0)
ex2 T λt2:T.eq T x (lift h d t2) λt2:T.pr3 e t2 t2
                   end of H4
                   we proceed by induction on H4 to prove pc3 e t1 t2
                      case ex_intro2 : x0:T H5:eq T x (lift h d x0) H6:pr3 e t2 x0 ⇒
                         the thesis becomes pc3 e t1 t2
                            (H7) 
                               by (pr3_gen_lift . . . . . H2 . H0)
ex2 T λt2:T.eq T x (lift h d t2) λt2:T.pr3 e t1 t2
                            end of H7
                            we proceed by induction on H7 to prove pc3 e t1 t2
                               case ex_intro2 : x1:T H8:eq T x (lift h d x1) H9:pr3 e t1 x1 ⇒
                                  the thesis becomes pc3 e t1 t2
                                     (H10) 
                                        we proceed by induction on H8 to prove eq T (lift h d x1) (lift h d x0)
                                           case refl_equal : ⇒
                                              the thesis becomes the hypothesis H5
eq T (lift h d x1) (lift h d x0)
                                     end of H10
                                     (H11) 
                                        by (lift_inj . . . . H10)
                                        we proved eq T x1 x0
                                        we proceed by induction on the previous result to prove pr3 e t1 x0
                                           case refl_equal : ⇒
                                              the thesis becomes the hypothesis H9
pr3 e t1 x0
                                     end of H11
                                     by (pc3_pr3_t . . . H11 . H6)
pc3 e t1 t2
pc3 e t1 t2
pc3 e t1 t2
          we proved pc3 e t1 t2
       we proved 
          ∀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)