proposition: Lemma map_union_mono_l {A} (m1 m2 m3 : M A) : m1 ⊆ m2 → m3 ∪ m1 ⊆ m3 ∪ m2.
proof: Proof. rewrite !map_subseteq_spec. intros ???. rewrite !lookup_union_Some_raw. naive_solver. Qed.
imports: Coq(Permutation) stdpp(options)