proposition: Lemma map_union_reflecting_l {A} (m1 m2 m3 : M A) : m3 ##ₘ m1 → m3 ##ₘ m2 → m3 ∪ m1 ⊆ m3 ∪ m2 → m1 ⊆ m2.
proof: Proof. rewrite !map_subseteq_spec. intros Hm31 Hm32 Hm i x ?. specialize (Hm i x). rewrite !lookup_union_Some in Hm by done. destruct Hm; auto. by rewrite map_disjoint_spec in Hm31; destruct (Hm31 i x x). Qed.
imports: Coq(Permutation) stdpp(options)