proposition: Lemma difference_insert {A} (m1 m2 : M A) i x1 x2 x3 : <[i:=x1]> m1 ∖ <[i:=x2]> m2 = m1 ∖ <[i:=x3]> m2.
proof: Proof. apply map_eq. intros i'. apply option_eq. intros x'. rewrite !lookup_difference_Some, !lookup_insert_Some, !lookup_insert_None. naive_solver. Qed.
imports: Coq(Permutation) stdpp(options)