proposition: Lemma elem_of_map_img_union_disjoint m1 m2 x : m1 ##ₘ m2 → x ∈ map_img (m1 ∪ m2) ↔ x ∈ map_img m1 ∨ x ∈ map_img m2.
proof: Proof. naive_solver eauto using elem_of_map_img_union, elem_of_map_img_union_l, elem_of_map_img_union_r. Qed.
imports: Coq(Permutation) stdpp(options)