proposition: Lemma singleton_1: forall x y, In y (singleton x) -> x=y.
proof: Proof. unfold singleton. intros x y. rewrite add_spec. unfold In. rewrite mem_Leaf. intuition discriminate. Qed.
imports: Bool PeanoNat BinPos OrderedType OrderedTypeEx FSetInterface