Add lemmas about the union and intersection of filters on maps

When merged, this merge request adds two new lemmas about the intersection and the union of filters on maps, as well as a supporting lemma about the intersection of lookups (such a supporting lemma already existed for unions, lookup_union). The proofs for the two primary lemmas were in part made with the help of Robbert.

To support the intersection of lookups, I had to create an instance of Intersection for the option type. This instance has the following behaviour:

• None ∩ None → None
• Some a ∩ None → None
• None ∩ Some b → None
• Some a ∩ Some b → Some a

This means that the intersection of option does not have a left identity. I am not sure if this is a problem.

added 1 commit

• ed4b34ad - Update CHANGELOG with changes

Compare with previous version

added 1 commit

• 24964b36 - Apply suggestions

Compare with previous version

resolved all threads

added 7 commits

• 24964b36...2febd0b9 - 6 commits from branch iris:master
• 22b167f9 - Merge branch 'master' into 'filter_union_intersection'

Compare with previous version

added 1 commit

• 26a2b067 - Update names of lemmas in CHANGELOG

Compare with previous version

added 1 commit

• 27aea16c - Add name to CHANGELOG

Compare with previous version

added 14 commits

• 27aea16c...ffe033d2 - 13 commits from branch iris:master
• 9c310148 - Merge branch 'master' into 'filter_union_intersection'

Compare with previous version

added 1 commit

• 138e0c4e - Turn implication into iff

Compare with previous version

mentioned in merge request !472 (merged)

added 1 commit

• edf623d5 - Apply 1 suggestion(s) to 1 file(s)

Compare with previous version

added 1 commit

• df2b045c - Apply 1 suggestion(s) to 1 file(s)

Compare with previous version