proposition: Lemma add_spec: forall x y s, In y (add x s) <-> x=y \/ In y s.
proof: Proof. unfold In. induction x; intros [y|y|] [|l o r]; simpl mem; try (rewrite IHx; clear IHx); rewrite ?mem_Leaf; intuition congruence. Qed.
imports: Bool PeanoNat BinPos OrderedType OrderedTypeEx FSetInterface