proposition: Lemma empty_in_iff : forall x, In x (empty elt) <-> False.
proof: Proof. unfold In. split; [intros (e,H); rewrite empty_mapsto_iff in H|]; intuition. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface