LocalAsGlobal Coq proofs accompanying our paper "Handling Local State with Global State" (submitted to MPC 2019).