Improve statement of aliasing theorem.
Separation properties alloc and free.
Separate separation stuff.