proposition: Lemma singleton_spec : forall x y, In y (singleton x) <-> y=x.
proof: Proof. unfold singleton. intros x y. rewrite add_spec. intuition. unfold In in *. rewrite mem_Leaf in *. discriminate. Qed.
imports: Bool PeanoNat BinPos Orders OrdersEx MSetInterface