proposition: Lemma elem_of_map_img_union_r m1 m2 x : m1 ##ₘ m2 → x ∈ map_img m2 → x ∈ map_img (m1 ∪ m2).
proof: Proof. intros. rewrite map_union_comm by done. by apply elem_of_map_img_union_l. Qed.
imports: Coq(Permutation) stdpp(options)