simp-normal form highlighting

[Julian]

Maybe it'd be nice (and reasonably easy?) to have a list of simp-normal forms and to highlight non-simp-normal terms as warnings.

Zulip and the docs have an existing list of these kinds of terms.