nat).(match hds with [PNil \Rightarrow PNil | (PCons h d hds0) \Rightarrow
(let j \def (trans hds0 i) in (let q \def (ptrans hds0 i) in (match (blt j d)
with [true \Rightarrow (PCons h (minus d (S j)) q) | false \Rightarrow
nat).(match hds with [PNil \Rightarrow PNil | (PCons h d hds0) \Rightarrow
(let j \def (trans hds0 i) in (let q \def (ptrans hds0 i) in (match (blt j d)
with [true \Rightarrow (PCons h (minus d (S j)) q) | false \Rightarrow