proposition: Lemma dom_empty_iff {A} (m : M A) : dom m ≡ ∅ ↔ m = ∅.
proof: Proof. split; [|intros ->; by rewrite dom_empty]. intros E. apply map_empty. intros. apply not_elem_of_dom. rewrite E. set_solver. Qed.
imports: stdpp(options)