proposition: Lemma elem_of_map (f : A → B) (X : C) y : y ∈ set_map (D:=D) f X ↔ ∃ x, y = f x ∧ x ∈ X.
proof: Proof. unfold set_map. rewrite elem_of_list_to_set, elem_of_list_fmap. by setoid_rewrite elem_of_elements. Qed.
imports: stdpp(relations) stdpp(options)