Simplify rewriting of events in `Pr` expressions

[jjanku]

Before #789 (v2025.10 and earlier), it was possible to easily rewrite events, for example, as follows:

require import AllCore.

module M = {
  proc run() : int = {
    return 1;
  }
}.

lemma l0 &m : Pr[M.run() @ &m : 0 <= res < 0] = 0%r.
proof.
rewrite (: forall x, (0 <= x < 0) = false).
+ smt().
by rewrite Pr[mu_false].
qed.

After #789, one has to, in general, use a combination of rewrite and byequiv (with conseq):

lemma l1 &m : Pr[M.run() @ &m : 0 <= res < 0] = 0%r.
proof.
rewrite (: Pr[M.run() @ &m: 0 <= res < 0] = Pr[M.run() @ &m: false]).
+ byequiv (_ : _ ==> true) => //.
  + sim.
  smt().
by rewrite Pr[mu_false].
qed.

See the changes to theories/modules/EventPartitioning.ec made by #789 for some more real-world examples.

It would be great if such rewriting of events was less verbose.

Also see the Zulip thread #EasyCrypt: dev > ✔ Cannot rewrite inside Pr in v2025.11 where I first reported this issue and where @fdupress suggested how this could be addressed.