proposition: Lemma dom_fmap {A B} (f : A → B) (m : M A) : dom (f <$> m) ≡ dom m.
proof: Proof. apply set_equiv. intros i. rewrite !elem_of_dom, lookup_fmap, <-!not_eq_None_Some. destruct (m !! i); naive_solver. Qed.
imports: stdpp(options)