proposition: Lemma map_img_singleton i x : map_img {[ i := x ]} ≡ {[ x ]}.
proof: Proof. apply set_equiv. intros y. rewrite elem_of_map_img. setoid_rewrite lookup_singleton_Some. set_solver. Qed.
imports: Coq(Permutation) stdpp(options)