--- /dev/null
+
+* In def 3.1 on p. 14, GS&V define `s` updated with \[[not φ]] as:
+
+ > { i &elem; s | i does not subsist in s[φ] }
+
+ where `i` *subsists* in <code>s[φ]</code> if there are any `i'` that *extend* `i` in <code>s[φ]</code>.
+
+ Here's how we can represent that:
+
+ <pre><code>bind_set s (fun (r, h) ->
+ let u = unit_set (r, h)
+ in let descendents = u >>= \[[φ]]
+ in if descendents = empty_set then u else empty_set
+ </code></pre>
+
+