proposition: Lemma dom_delete {A} (m : M A) i : dom (delete i m) ≡ dom m ∖ {[ i ]}.
proof: Proof. apply set_equiv. intros j. rewrite elem_of_difference, !elem_of_dom. unfold is_Some. setoid_rewrite lookup_delete_Some. set_solver. Qed.
imports: stdpp(options)