[Haskell-cafe] Proving stuff about IORefs

I have a formal proof where I am stuck at a certain point. Suppose we have a function f :: IORef a -> IO b I want to prove that f r == do s1 <- readIORef r r' <- newIORef s1 x <- f r' s3 <- readIORef r' writeIORef r s3 return x What happens here is that the temporary IORef r' takes the place of the argument r, and after we apply f to it we take its content and store it in the original r. This should be the same as using r as argument to f in the first place. How can I prove this formally? Cheers Ben