proposition: Lemma dom_alter {A} f (m : M A) i : dom (alter f i m) ≡ dom m.
proof: Proof. apply set_equiv; intros j; rewrite !elem_of_dom; unfold is_Some. destruct (decide (i = j)); simplify_map_eq/=; eauto. destruct (m !! j); naive_solver. Qed.
imports: stdpp(options)