proposition: Lemma set_bind_disj_union_L `{!LeibnizEquiv SB} f (X Y : C) : X ## Y → set_bind f (X ∪ Y) = set_bind f X ∪ set_bind f Y.
proof: Proof. unfold_leibniz. apply set_bind_disj_union. Qed.
imports: stdpp(relations) stdpp(options)