DEFINITION PList_rec()
TYPE =
       ΠP:PList→Set
         .P PNil
           →(Πn:nat.Πn1:nat.Πp:PList.(P p)→(P (PCons n n1 p))
                →Πp:PList.(P p))
BODY =
Show proof