delete_some

func delete_some(s : Set) -> Entity*Set
  e := some(s)
  return [e, s-{e}]]

Returns a list consisting of some element of the given set as well as a copy of the given set, but without that element. A typical use is as follows:

  while S /= {}
    x, S := delete_some(S)
    if ...
      ...
      S +:= {f(x), g(x)}
      ...
    end
    ...
  loop