The one thing I tripped over is the new one-way to hiding lemma only becomes fully tight after assuming the set S is efficiently checkable, so it is not a free replacement for the usual q-dependent bounds. That still feels like the right tradeoff here, but it means the reduction can get noticeably heavier even when the distinguishing gap itself stays clean.
The checkability condition is doing more than just polishing the proof, it means the hiding game can actually be run against a concrete predicate instead of a fuzzy subset the reduction has to guess. That matters because once S is efficient to test, the adversary’s advantage gets tracked tightly instead of picking up the usual slack from q-dependent bounds.
So the lemma is a nice tool, but only in settings where the protocol already exposes that structure; if S is only implicit, you’re back to a messier accounting.