DEFINITION drop1_gen_pnil()
TYPE =
       ∀c1:C.∀c2:C.(drop1 PNil c1 c2)→(eq C c1 c2)
BODY =
        assume c1: C
        assume c2: C
        suppose H: drop1 PNil c1 c2
           assume y: PList
           suppose H0: drop1 y c1 c2
             we proceed by induction on H0 to prove (eq PList y PNil)→(eq C c1 c2)
                case drop1_nil : c:C ⇒
                   the thesis becomes (eq PList PNil PNil)→(eq C c c)
                      suppose : eq PList PNil PNil
                         by (refl_equal . .)
                         we proved eq C c c
(eq PList PNil PNil)→(eq C c c)
                case drop1_cons : c3:C c4:C h:nat d:nat :drop h d c3 c4 c5:C hds:PList :drop1 hds c4 c5 ⇒
                   the thesis becomes ∀H4:(eq PList (PCons h d hds) PNil).(eq C c3 c5)
                   () by induction hypothesis we know (eq PList hds PNil)→(eq C c4 c5)
                      suppose H4: eq PList (PCons h d hds) PNil
                         (H5) 
                            we proceed by induction on H4 to prove <λ:PList.Prop> CASE PNil OF PNil⇒False | PCons   ⇒True
                               case refl_equal : ⇒
                                  the thesis becomes <λ:PList.Prop> CASE PCons h d hds OF PNil⇒False | PCons   ⇒True
                                     consider I
                                     we proved True
<λ:PList.Prop> CASE PCons h d hds OF PNil⇒False | PCons   ⇒True
<λ:PList.Prop> CASE PNil OF PNil⇒False | PCons   ⇒True
                         end of H5
                         consider H5
                         we proved <λ:PList.Prop> CASE PNil OF PNil⇒False | PCons   ⇒True
                         that is equivalent to False
                         we proceed by induction on the previous result to prove eq C c3 c5
                         we proved eq C c3 c5
∀H4:(eq PList (PCons h d hds) PNil).(eq C c3 c5)
             we proved (eq PList y PNil)→(eq C c1 c2)
          we proved ∀y:PList.(drop1 y c1 c2)→(eq PList y PNil)→(eq C c1 c2)
          by (insert_eq . . . . previous H)
          we proved eq C c1 c2
       we proved ∀c1:C.∀c2:C.(drop1 PNil c1 c2)→(eq C c1 c2)