Add a number of missing intersection lemmas

This pull request adds a number of missing lemmas about the intersection on options (closes #166 (closed)). The lookup_intersection lemma was added in !466 (merged).