proposition: Lemma find_o : forall m x y, E.eq x y -> find x m = find y m.
proof: Proof. intros. rewrite eq_option_alt. intro e. rewrite <- 2 find_mapsto_iff. apply MapsTo_iff; auto. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface