proposition: Lemma inter_empty a b : inter a b [=] empty <-> (forall x, In x a -> ~In x b).
proof: Proof. split; intro h. intros x h1 h2. rewrite <- empty_iff with (x:=x), <- h. apply inter_3; hyp. intro x. set_iff. fo. Qed.
imports: Coq(FSets) CoLoR(LogicUtil RelUtil BoolUtil)