linter.fugue.byExact

by exact e in term position is e. by classical exact e is e when e does not actually need the classical instance — and when it does, classical belongs further up (an open Classical in on the enclosing declaration, or a classical hoisted above the branch that needs it), not wrapped around a single exact.

The inner term is re-elaborated against the goal before the by block ran — for the classical case that context has no extra instance, so a success means classical did nothing here.