Commit 2026-06-02 14:56 f764b0e8

fix: use notation3 more (#39383)

• notation3 is better at generating delaborators in the presence of implicit arguments, other notation and some other complications.
• I explicitly tested that each change was not correctly pretty-printed before, but now is.
• Add spaces around the global notation ^+ (that maybe shouldn't be global at all?)