There are two redexes in this term; we've marked the operative lambdas
with a star. If we reduce the leftmost redex first, the term reduces
-to the normal form `I` in one step. But if we reduce the left most
+to the normal form `I` in one step. But if we reduce the rightmost
redex instead, the "reduced" form is `(\x.I)Ω` again, and we are in
danger of entering an infinite loop.