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.