A couple of clear, encouraging, articles about how to use TLA and the benefits it provides would pay dividends (to both you and your readers) orders of magnitude greater than this obscure, roundabout, oblique approach.

> This confuses some people to believe that TLA+ doesn't support higher-order algorithms, when, in fact, it becomes a non-issue.

An article explaining this would be astonishingly interesting (and probably clarify this whole discussion).