proposition: Lemma exists_empty : exists_ f empty = false.
proof: Proof. assert (forall b, b = false <-> ~b=true). clear. intros [|]; firstorder. congruence. rewrite H. clear H. intro. rewrite <- exists_iff in H. destruct H. setdec. apply Hcompat. Qed.
imports: Coq(FSets) ATBR(Common) ATBR(BoolView)