proposition: Lemma map_difference_union {A} (m1 m2 : M A) : m1 ⊆ m2 → m1 ∪ m2 ∖ m1 = m2.
proof: Proof. rewrite map_subseteq_spec. intro Hm1m2. apply map_eq. intros i. apply option_eq. intros v. specialize (Hm1m2 i). unfold difference, map_difference, difference_with, map_difference_with. rewrite lookup_union_Some_raw, lookup_merge. destruct (m1 !! i) as [x'|], (m2 !! i); try specialize (Hm1m2 x'); compute; intuition congruence. Qed.
imports: Coq(Permutation) stdpp(options)