A SERVICE OF

logo

12.7. SETS 99
==> (ITSET f EMPTY b = b) /\
(!x s.
FINITE s
==> (ITSET f (x INSERT s) b =
if x IN s then ITSET f s b else f x (ITSET f s b)))