proposition: Lemma empty_a : forall x, mem x (empty elt) = false.
proof: Proof. intros. case_eq (mem x (empty elt)); intros; auto. generalize (mem_2 H). rewrite empty_in_iff; intuition. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface