proposition: Lemma dom_union {A} (m1 m2 : M A) : dom (m1 ∪ m2) ≡ dom m1 ∪ dom m2.
proof: Proof. apply set_equiv. intros i. rewrite elem_of_union, !elem_of_dom. unfold is_Some. setoid_rewrite lookup_union_Some_raw. destruct (m1 !! i); naive_solver. Qed.
imports: stdpp(options)