Haddocks for normal forms of boolean expressions

[langston-barrett]

          I would argue that we should spell out the expectations for how boolean normalization should work here in the library Haddocks, not tucked away in the comments of a test suite. Do you agree?

Originally posted by @RyanGlScott in #277 (comment)

The task is to take the comments in test/Bool.hs and turn them into a comprehensive, numbered list of invariants. The checks in Bool.hs should then refer to the invariants by number. Above isNormal and below the list of invariants, we should put comments requesting that developers keep them in sync.

We should also note the motivation for these rewrites / normal forms: to reduce the sizes of terms, to keep terms more concrete, and (in the service of the first two) to keep terms in normal forms (e.g., so that they can be compared for equality, and rewrite rules can assume normal forms as inputs). We should describe how each invariant contributes to these goals.