let bind in the shrink pass

book.tex

@@ -3484,7 +3484,8 @@ expressible in terms of addition and negation.
 Several of the comparison operations are expressible in terms of
 less-than and logical negation.
 \[
-  (\key{<=}\; e_1 \; e_2) \quad \Rightarrow \quad (\key{not}\;(\key{<}\;e_2\;e_1))
+(\key{<=}\; e_1 \; e_2) \quad \Rightarrow \quad
+\LET{t_1}{e_1}{(\key{not}\;(\key{<}\;e_2\;t_1))}
 \]
 By performing these translations near the front-end of the compiler,
 the later passes of the compiler will not need to deal with these