proposition: Lemma map_disjoint_union_r {A} (m1 m2 m3 : M A) : m1 ##ₘ m2 ∪ m3 ↔ m1 ##ₘ m2 ∧ m1 ##ₘ m3.
proof: Proof. rewrite !map_disjoint_alt. setoid_rewrite lookup_union_None. naive_solver. Qed.
imports: Coq(Permutation) stdpp(options)