proposition: Lemma elem_of_map_img_union m1 m2 x : x ∈ map_img (m1 ∪ m2) → x ∈ map_img m1 ∨ x ∈ map_img m2.
proof: Proof. rewrite !elem_of_map_img. setoid_rewrite lookup_union_Some_raw. naive_solver. Qed.
imports: Coq(Permutation) stdpp(options)