proposition: Lemma map_img_insert m i x : map_img (<[i:=x]> m) ≡ {[ x ]} ∪ map_img (delete i m).
proof: Proof. intros y. rewrite elem_of_union, !elem_of_map_img, elem_of_singleton. setoid_rewrite lookup_delete_Some. setoid_rewrite lookup_insert_Some. naive_solver. Qed.
imports: Coq(Permutation) stdpp(options)