Proved Store! Hurray!

As expected, this one was "fun". Ssreflect's library on paths was extremely
helpful. Fixed an error that I had introduced in the invariant when I translated
it from Reachability.v.