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 *) ```