Richard Eisenberg authored Mar 17, 2020 and Marge Bot committed Mar 20, 2020

Key changes:
 * Adds a new rule for forall-coercions over coercion variables, which
was implemented but conspicuously missing from the spec.
 * Adds treatment for FunCo.
 * Adds treatment for ForAllTy over coercion variables.
 * Improves commentary (including restoring a Note lost in
03d48526) in the source.

No changes to running code.