proposition: Lemma mem_b : forall m x y, E.eq x y -> mem x m = mem y m.
proof: Proof. intros. generalize (mem_in_iff m x) (mem_in_iff m y)(In_iff m H). destruct (mem x m); destruct (mem y m); intuition. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface