Prototype Implementation of Rely-Guarantee References as a Coq DSL