proposition: Lemma dom_insert {A} (m : M A) i x : dom (<[i:=x]>m) ≡ {[ i ]} ∪ dom m.
proof: Proof. apply set_equiv. intros j. rewrite elem_of_union, !elem_of_dom. unfold is_Some. setoid_rewrite lookup_insert_Some. destruct (decide (i = j)); set_solver. Qed.
imports: stdpp(options)