Add an ensures to memmove()

The first n bytes of the source and destination objects being disjoint is
a sufficient condition to conclude that the source was not changed as a
result of the copy operation.