when rnd{1} and rnd{2} are given arguments, an error message is needed

[alleystoughton]

In 1.0, one can give rnd{1} and rnd{2} arguments (which are ignored and not even typechecked). Instead, an error message should be issued.

[oskgo]

Triage: This still reproduces

MRE:

require import DBool.

module Foo = {
  proc foo() = {
    var b;
    b <$ {0,1};
  }
}.

equiv L: Foo.foo ~ Foo.foo: true ==> true.
proof.
proc.
rnd{1} ignored.