proposition: Lemma map_compose_empty_iff_dom_img {C} `{FinMap K' M', !RelDecision (∈@{D})} (m : M C) (n : M' K) : m ∘ₘ n = ∅ ↔ dom m ## map_img n.
proof: Proof. rewrite map_compose_empty_iff, elem_of_disjoint. setoid_rewrite elem_of_dom. setoid_rewrite eq_None_not_Some. setoid_rewrite elem_of_map_img. naive_solver. Qed.
imports: stdpp(options)