proposition: Lemma set_map_union_L `{!LeibnizEquiv D} (f : A → B) (X Y : C) : set_map (D:=D) f (X ∪ Y) = set_map (D:=D) f X ∪ set_map (D:=D) f Y.
proof: Proof. unfold_leibniz. apply set_map_union. Qed.
imports: stdpp(relations) stdpp(options)