DEFINITION PList_rect()
TYPE =
       ΠP:PList
                →(Type:85924:cic:/matita/LAMBDA-TYPES/Base-1/plist/defs/PList_rect.con)
         .P PNil
           →(Πn:nat.Πn1:nat.Πp:PList.(P p)→(P (PCons n n1 p))
                →Πp:PList.(P p))
BODY =
Show proof