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