`simp_mem` failure with `GCMGmultV8`

[shigoel]

Ref.: #153

See here: simp_mem creates a malformed term under the hood, forcing the user to manually rewrite with Memory.read_bytes_write_bytes_eq_read_bytes_of_mem_separate'.

[shigoel]

Update: note that simp_mem fails only for the proof obligation

    -- HTable is unmodified.
    sf[read_gpr 64 1#5 s0, 256] = HTable

For the more general obligation (which subsumes the above), simp_mem works fine.

  MEM_UNCHANGED_EXCEPT [(r (.GPR 0) s0, 128)] (sf, s0)