* Now how shall we handle \[[∃x]]. As we said, GS&V really tell us how to interpret \[[∃xPx]], but what they say about this breaks naturally into two pieces, such that we can represent the update of `s` with \[[∃xPx]] as:
-<pre><code>
-s >>= \[[∃x]] >>= \[[Px]]
-</code></pre>
+ <pre><code>
+ s >>= \[[∃x]] >>= \[[Px]]
+ </code></pre>