`symmetry` fails to carry local variables to their new side

[fdupress]

module M = {
  proc f() = {
    var f : int;

    f <- 0;
  }

  proc g() = {}
}.

equiv toto: M.f ~ M.g: true ==> ={res}.
proof.
proc. symmetry.

yields

Current goal

Type variables: <none>

------------------------------------------------------------------------------------------------------------------
&1 (left ) : {f : int}
&2 (right) : {}

pre = true

                           (1)  f <- 0                   

post = tt = tt

(Note that the memory type has f in the left memory.)