Two requirements to add to the list of internal invariants:

• During the lifetime 'a, no code will access* this memory region treating UnsafeCells as existing at different ranges than they exist in T
• During the lifetime 'a, no reference will exist to this memory which treats UnsafeCells as existing at different ranges than they exist in T

• What does "access" mean? Should this just say "loads and stores"?