let rec trans (hds: PList) on hds: nat \to nat \def \lambda (i: nat).(match
hds with [PNil \Rightarrow i | (PCons h d hds0) \Rightarrow (let j \def
let rec trans (hds: PList) on hds: nat \to nat \def \lambda (i: nat).(match
hds with [PNil \Rightarrow i | (PCons h d hds0) \Rightarrow (let j \def