Equivalents of the definitional equality rules are applied to simplify programs, with inlining again playing a major role.
