proposition: Lemma empty_o : forall x, find x (empty elt) = None.
proof: Proof. intros. rewrite eq_option_alt. intro e. rewrite <- find_mapsto_iff, empty_mapsto_iff; now intuition. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface