-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
-(trans hds0 i) in (let TMP_1 \def (blt j d) in (match TMP_1 with [true
-\Rightarrow j | false \Rightarrow (plus j h)])))]).
+rec definition 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 (trans hds0 i) in (match (blt j d) with [true \Rightarrow j | false
+\Rightarrow (plus j h)]))]).