The refinement relation on addresses allows union references to be refined:

  (β2 → β1) → RUnion i s β1 ⊆ RUnion i s β2

The result is that frozen values are below their unfrozen variant, which made
it possible to prove that constant propagation (see constant_propagation.v) can
be performed on the level of the memory model.