proposition: Lemma map_subseteq_union {A} (m1 m2 : M A) : m1 ⊆ m2 → m1 ∪ m2 = m2.
proof: Proof. rewrite map_subseteq_spec. intros Hm1m2. apply map_eq. intros i. apply option_eq. intros x. rewrite lookup_union_Some_raw. split; [by intuition |]. intros Hm2. specialize (Hm1m2 i). destruct (m1 !! i) as [y|]; [| by auto]. rewrite (Hm1m2 y eq_refl) in Hm2. intuition congruence. Qed.
imports: Coq(Permutation) stdpp(options)