We extend a Coq formalization of monadic equational reasoning with a monad to represent typed stores. This leads us to design an original equational theory, that we experimented on a number of examples. The examples themselves are generated from OCaml programs using an experimental compiler from OCaml to Coq, which targets the typed store monad.