We should have lookup_intersection and the lemmas from !432 (merged) for intersection.
lookup_intersection