Arthur-Merlin protocol with BQP power
I'm glad you're interested in my IP with BQP prover problem!

Unfortunately, I'm not sure I understand your question.  If the function $f$ satisfies the Simon promise, then Merlin can easily convince Arthur of that by telling him the secret string $s$.  If, on the other hand, $f$ is one-to-one, then Merlin can convince himself of that (by using Simon's algorithm to look for $s$ and not finding anything), but the question is how he can convince Arthur.  It clearly won't do for Merlin to say, "Arthur, I looked for $s$, but I found nuthin'!"  For how would Arthur know that Merlin wasn't lying?

Now, it's a known theorem that, if Merlin wasn't around, then Arthur would need to make at least ~$2^{n/2}$ black-box queries to $f$, in order to decide with high probability whether $f$ was one-to-one or satisfied the Simon promise.

It's also known that, if Merlin had unbounded computational power (not just the power of BQP), then there is an interactive protocol by which Merlin could convince Arthur that $f$ is one-to-one.  Namely, Arthur picks a random $x$, evaluates $f(x)$, sends $f(x)$ to Merlin, and asks Merlin to tell him what $x$ was.  If $f$ is one-to-one, then Merlin---provided he has NP search powers---can always answer such challenges correctly.  But if $f$ is two-to-one, then Merlin must be wrong with probability at least $1/2$.

The case I asked about---the one where Merlin has BQP powers, but no more than that---is still open.

To answer your last question: no, one would not need to prove BPP&ne;BQP in order to solve this problem.  The reason is that this problem only concerns the relativized setting: the setting where the function $f$ is a black box, which Arthur and Merlin can learn about only by querying it.  And in the relativized setting---unlike the "real," unrelativized one---we can often prove unconditional separations between complexity classes!  Indeed, I already mentioned one example above: it's known that any classical randomized algorithm to solve Simon's problem has to make exponentially many queries to $f$.  That fact implies the existence of an oracle separating BPP from BQP.