proposition: Lemma add_eq_b : forall m x y e, E.eq x y -> mem y (add x e m) = true.
proof: Proof. intros; rewrite mem_find_b; rewrite add_eq_o; auto. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface