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