proposition: Lemma is_empty_eq s : is_empty s = true <-> s [=] empty.
proof: Proof. split; intro hs. apply empty_is_empty_1. rewrite is_empty_iff. hyp. rewrite <- is_empty_iff. apply empty_is_empty_2. hyp. Qed.
imports: Coq(FSets) CoLoR(LogicUtil RelUtil BoolUtil)