* 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 s[φ]
if there are any `i'` that *extend* `i` in s[φ]
.
Here's how we can represent that:
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