Yeah, a predictor won't necessarily figure out every true statement, but my original point was about the transparent Newcomb's, in which case if Omega finds that the agent one-boxes whenever Omega fills both boxes, then Omega will fill both and the agent will one-box.

In the case of the proof-searching model things aren't quite as nice, but you can still get pretty far. If the predictor has a sufficiently high proof limit and knows that it fills both boxes whenever it finds a proof of one-boxing, then a short enough proof that the agent one-boxes whenever both boxes are filled should be sufficient (I'm quite sure a Löbian argument holds here).

So yes, from the predictor's point of view, a proof that the agent one-boxes whenever both boxes are filled should be sufficient. Now you just need the agent to not be stupid...