* Parametrize refinements with memories. This way, refinements imply typing,
  for example [w1 ⊑{Γ,f@m1↦m2} w2 : τ → (Γ,m1) ⊢ w1 : τ]. This relieves us from
  various hacks.
* Use addresses instead of index/references pairs for lookup and alter
  operations on memories.
* Prove various disjointness properties.