proposition: Lemma add_iff : In y (add x s) <-> E.eq x y \/ In y s.
proof: Proof. split; [ | destruct 1; [apply add_1|apply add_2]]; auto. destruct (eq_dec x y) as [E|E]; auto. intro H; right; exact (add_3 E H). Qed.
imports: DecidableTypeEx FSetInterface