Missing documentation for simplification

[asr]

The CHANGELOG says:

* Key bindings for controlling simplification/normalisation:

  [TODO: Simplification should be explained somewhere.]

  Commands like `Goal type and context` (`C-c C-,`) could previously
  be invoked in two ways. By default the output was normalised, but if
  a prefix argument was used (for instance via `C-u C-c C-,`), then no
  explicit normalisation was performed. Now there are three options:

  - By default (`C-c C-,`) the output is simplified.

  - If `C-u` is used exactly once (`C-u C-c C-,`), then the result is
    neither (explicitly) normalised nor simplified.

  - If `C-u` is used twice (`C-u C-u C-c C-,`), then the result is
    normalised.

So, the documentation for simplification is missing.