-definition trans:
- PList \to (nat \to nat)
-\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 (trans hds0 i) in (match (blt j d) with [true \Rightarrow j | false
-\Rightarrow (plus j h)]))])) in trans.
+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)])))]).