DEFINITION PConsTail()
TYPE =
       PList→nat→nat→PList
BODY =
FIXPConsTail{
         PConsTail:PList→nat→nat→PList
         :=λhds:PList
           .λh0:nat
             .λd0:nat
               .<λp:PList.PList>
                 CASE hds OF
                   PNil⇒PCons h0 d0 PNil
                 | PCons h d hds0⇒PCons h d (PConsTail hds0 h0 d0)
         }