Mechanizing Local Reasoning with Contexts