let rec PConsTail (hds: PList) on hds: nat \to (nat \to PList) \def \lambda
(h0: nat).(\lambda (d0: nat).(match hds with [PNil \Rightarrow (PCons h0 d0
let rec PConsTail (hds: PList) on hds: nat \to (nat \to PList) \def \lambda
(h0: nat).(\lambda (d0: nat).(match hds with [PNil \Rightarrow (PCons h0 d0