proposition: Lemma mem_node: forall x l o r, mem x (node l o r) = mem x (Node l o r).
proof: Proof. intros x l o r. case o; trivial. destruct l; trivial. destruct r; trivial. now destruct x. Qed.
imports: Bool PeanoNat BinPos OrderedType OrderedTypeEx FSetInterface