Previously, we have seen how to use logical replacement rules in isolation. This lecture uses a succession of replacement rules to turn a very ugly statement into a very clean and digestible one.
In the process, we get a flavor of proofs, which will be the main topic two units from now.