proposition: Lemma map_disjoint_dom {A} (m1 m2 : M A) : m1 ##ₘ m2 ↔ dom m1 ## dom m2.
proof: Proof. rewrite map_disjoint_spec, elem_of_disjoint. setoid_rewrite elem_of_dom. unfold is_Some. naive_solver. Qed.
imports: stdpp(options)