linter.fugue.firstVsSolve

A first | … in terminal position — the last tactic of a by / · / { } / case arm — must have closed the goal in a compiling proof, so it is a solve | …: solve errors if a branch succeeds without closing, first does not.

<;> first and blanket-selector forms are seqFocusPipe / selectorFirst's, not this one.