DEFINITION PList_ind()
TYPE =
       ∀P:PList→Prop
         .P PNil
           →(∀n:nat.∀n1:nat.∀p:PList.(P p)→(P (PCons n n1 p)))→∀p:PList.(P p)
BODY =
        assume P: PList→Prop
        suppose H: P PNil
        suppose H1: ∀n:nat.∀n1:nat.∀p:PList.(P p)→(P (PCons n n1 p))
          (aux) by well-founded reasoning we prove ∀p:PList.(P p)
          assume p: PList
             by cases on p we prove P p
                case PNil ⇒
                   the thesis becomes the hypothesis H
                case PCons n:nat n1:nat p1:PList ⇒
                   the thesis becomes P (PCons n n1 p1)
                   by (aux .)
                   we proved P p1
                   by (H1 . . . previous)
P (PCons n n1 p1)
             we proved P p
∀p:PList.(P p)
          done
          consider aux
          we proved ∀p:PList.(P p)
       we proved 
          ∀P:PList→Prop
            .P PNil
              →(∀n:nat.∀n1:nat.∀p:PList.(P p)→(P (PCons n n1 p)))→∀p:PList.(P p)