* 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