proposition: Lemma map_img_union_disjoint m1 m2 : m1 ##ₘ m2 → map_img (m1 ∪ m2) ≡ map_img m1 ∪ map_img m2.
proof: Proof. intros Hdisj. apply set_equiv. intros x. rewrite elem_of_union. by apply elem_of_map_img_union_disjoint. Qed.
imports: Coq(Permutation) stdpp(options)