confusing error message on memory rewrite attempt

A memory isn't (and doesn't represent) an equality, so there is no expectation that a rewrite should work, but memories get renamed to `_` sometimes when they are unused, and this can lead to confusing error messages.

```
module type MT = {}.

lemma L (M<: MT):forall &m, (glob M){m}=witness => true.
proof.
move => <-. (* memory is renamed to `_` before it is put into error message *)
```