proposition: Lemma mem_spec : forall x s, reflect (In x s) (mem x s).
proof: Proof. intros. case_eq (mem x s); intro H; constructor. apply mem_2. assumption. intro H'. apply mem_1 in H'. rewrite H in H'. discriminate. Qed.
imports: Coq(FSets) ATBR(Common) ATBR(BoolView)