Skip to content

Add lemmas `set_fold_union_strong` and `set_fold_union`.

Robbert Krebbers requested to merge robbert/set_fold_union into master

This discussion at Mattermost nerdsniped me to add the lemma set_fold_union and the stronger lemma set_fold_union_strong that only requires idempotence/associativity/commutativity for the elements in the sets.

Interestingly, the already existing "disjoint" versions of the lemma can be derived.

The proofs are pretty long/tricky, so I tried to add some comments what's going on.

Merge request reports