DEFINITION drop1_trans()
TYPE =
       ∀is1:PList.∀c1:C.∀c0:C.(drop1 is1 c1 c0)→∀is2:PList.∀c2:C.(drop1 is2 c0 c2)→(drop1 (papp is1 is2) c1 c2)
BODY =
       assume is1: PList
          we proceed by induction on is1 to prove ∀c1:C.∀c0:C.(drop1 is1 c1 c0)→∀is2:PList.∀c2:C.(drop1 is2 c0 c2)→(drop1 (papp is1 is2) c1 c2)
             case PNil : ⇒
                the thesis becomes ∀c1:C.∀c0:C.(drop1 PNil c1 c0)→∀is2:PList.∀c2:C.(drop1 is2 c0 c2)→(drop1 (papp PNil is2) c1 c2)
                    assume c1: C
                    assume c0: C
                    suppose H: drop1 PNil c1 c0
                    assume is2: PList
                    assume c2: C
                    suppose H0: drop1 is2 c0 c2
                      (H_y) 
                         by (drop1_gen_pnil . . H)
eq C c1 c0
                      end of H_y
                      (H1) 
                         by (eq_ind_r . . . H0 . H_y)
drop1 is2 c1 c2
                      end of H1
                      consider H1
                      we proved drop1 is2 c1 c2
                      that is equivalent to drop1 (papp PNil is2) c1 c2
∀c1:C.∀c0:C.(drop1 PNil c1 c0)→∀is2:PList.∀c2:C.(drop1 is2 c0 c2)→(drop1 (papp PNil is2) c1 c2)
             case PCons : n:nat n0:nat p:PList ⇒
                the thesis becomes ∀c1:C.∀c0:C.∀H0:(drop1 (PCons n n0 p) c1 c0).∀is2:PList.∀c2:C.∀H1:(drop1 is2 c0 c2).(drop1 (PCons n n0 (papp p is2)) c1 c2)
                (H) by induction hypothesis we know ∀c1:C.∀c0:C.(drop1 p c1 c0)→∀is2:PList.∀c2:C.(drop1 is2 c0 c2)→(drop1 (papp p is2) c1 c2)
                    assume c1: C
                    assume c0: C
                    suppose H0: drop1 (PCons n n0 p) c1 c0
                    assume is2: PList
                    assume c2: C
                    suppose H1: drop1 is2 c0 c2
                      (H_x) 
                         by (drop1_gen_pcons . . . . . H0)
ex2 C λc2:C.drop n n0 c1 c2 λc2:C.drop1 p c2 c0
                      end of H_x
                      (H2) consider H_x
                      we proceed by induction on H2 to prove drop1 (PCons n n0 (papp p is2)) c1 c2
                         case ex_intro2 : x:C H3:drop n n0 c1 x H4:drop1 p x c0 ⇒
                            the thesis becomes drop1 (PCons n n0 (papp p is2)) c1 c2
                               by (H . . H4 . . H1)
                               we proved drop1 (papp p is2) x c2
                               by (drop1_cons . . . . H3 . . previous)
drop1 (PCons n n0 (papp p is2)) c1 c2
                      we proved drop1 (PCons n n0 (papp p is2)) c1 c2
                      that is equivalent to drop1 (papp (PCons n n0 p) is2) c1 c2
∀c1:C.∀c0:C.∀H0:(drop1 (PCons n n0 p) c1 c0).∀is2:PList.∀c2:C.∀H1:(drop1 is2 c0 c2).(drop1 (PCons n n0 (papp p is2)) c1 c2)
          we proved ∀c1:C.∀c0:C.(drop1 is1 c1 c0)→∀is2:PList.∀c2:C.(drop1 is2 c0 c2)→(drop1 (papp is1 is2) c1 c2)
       we proved ∀is1:PList.∀c1:C.∀c0:C.(drop1 is1 c1 c0)→∀is2:PList.∀c2:C.(drop1 is2 c0 c2)→(drop1 (papp is1 is2) c1 c2)