-(let j \def (trans hds0 i) in (let q \def (ptrans hds0 i) in (let TMP_1 \def
-(blt j d) in (match TMP_1 with [true \Rightarrow (let TMP_2 \def (S j) in
-(let TMP_3 \def (minus d TMP_2) in (PCons h TMP_3 q))) | false \Rightarrow
-q]))))]).
+(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
+q])))]).