MEVALP1 leaking assumption



Not sure I understand what you're proposing. Won't that break

    [ asksign(x), sign(x), sign(x) ] ?

The scope of asksign is supposed to be one top-level interaction.

          -s