redex instead, the "reduced" form is `(\x.I)Ω` again, and we are in
danger of entering an infinite loop.
-Thanks to the recent introduction of sum types (disjoint union), we
+Thanks to the introduction of sum types (disjoint union) in the last lecture, we
are now in a position to gain a deeper understanding of evaluation
order by reasoning explicitly about evaluation by writing a program
that evaluates terms.