rw and similar when applied to bounded rewrites -- behaviour unconscionable

[mn200]

Consider different behaviours of these three:

rw[Once FUNPOW] ([], ``p (FUNPOW f (SUC n) x) /\ q (FUNPOW g (SUC n) y)``);
simp[Once FUNPOW] ([], ``p (FUNPOW f (SUC n) x) /\ q (FUNPOW g (SUC n) y)``);
(conj_tac >> simp[Once FUNPOW]) ([], ``p (FUNPOW f (SUC n) x) /\ q (FUNPOW g (SUC n) y)``);

First rewrites in the last conjunct; second rewrites in the first, and last rewrites in both. Given that rw is doing a rpt conj_tac before performing any simplification, I think it should emulate the last one and have the rewrite apply once each in every conjunct.

Particularly painfully: the behaviour of the first is not even predictable if THEN is concurrent, as per #575.