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 =
λP:PList→Set
         .λ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)
               }