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 =
Show proof