Applying rule 2 again we get this pretty version
Normally, you would not apply the substitution rules to get this final version. You would just write it. I have used the rules here to emphasize that the imperative-style thinking that comes naturally with do blocks is actually based on monadic expressions. It's a bit amazing isn't it?