The fold operation for a commutative associative operation over a finset. #
A stronger version of
Finset.fold_ite, but relies on
an explicit proof of idempotency on the seed element, rather
than relying on typeclass idempotency over the whole type.
A weaker version of
relying on typeclass idempotency over the whole type,
instead of solely on the seed element.
However, this is easier to use because it does not generate side goals.