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