Prerequisites

We're going to lift the memory operations and theorems from a base type bmem to a "richer" type mem, which contains bmem as a component. Formally, this means that we have a Lens mem bmem which provides us with well-behaved accessors to the bmem component inside of mem. While this is enough to lift most of the memory operations and theorems, we also need to know the value of the empty memory state of the richer type mem; indeed there's no way we would be able to construct that just from empty : bmem. However, the simpler memory state contained within this empty mem should correspond to the empty bmem from the base memory states.