proposition: Lemma dom_map_zip_with {A B C} (f : A → B → C) (ma : M A) (mb : M B) : dom (map_zip_with f ma mb) ≡ dom ma ∩ dom mb.
proof: Proof. rewrite set_equiv. intros x. rewrite elem_of_intersection, !elem_of_dom, map_lookup_zip_with. destruct (ma !! x), (mb !! x); rewrite !is_Some_alt; naive_solver. Qed.
imports: stdpp(options)