proposition: Lemma delete_difference {A} (m1 m2 : M A) i x : delete i (m1 ∖ m2) = m1 ∖ <[i:=x]> m2.
proof: Proof. apply map_eq. intros j. apply option_eq. intros y. rewrite lookup_delete_Some, !lookup_difference_Some, lookup_insert_None. naive_solver. Qed.
imports: Coq(Permutation) stdpp(options)