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 =
λP:PList
               →(Type:85924:cic:/matita/LAMBDA-TYPES/Base-1/plist/defs/PList_rect.con)
         .λp:P PNil
           .λf:Πn:nat.Πn1:nat.Πp1:PList.(P p1)→(P (PCons n n1 p1))
             .FIXaux{
               aux:Πp1:PList.(P p1)
               :=λp1:PList.<P> CASE p1 OF PNil⇒p | PCons n n1 p2⇒f n n1 p2 (aux p2)
               }