Exposed memories from rewrites

When rewriting using an assumption with a memory parameter the generated goals don't include the memory into the context.

In many cases trying to rewrite using an assumption with a memory parameter fails, but I found a working example:

```
module type MT = {}.

lemma L (M<: MT):(forall &m, (glob M){m}=witness => true) => 
  true.
proof.
move => ->. (* exposes memory outside context *)
abort.
```