proposition: Lemma elements_o : forall m x, find x m = findA (eqb x) (elements m).
proof: Proof. intros. rewrite eq_option_alt. intro e. rewrite <- find_mapsto_iff, elements_mapsto_iff. unfold eqb. rewrite <- findA_NoDupA; dintuition; try apply elements_3w; eauto. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface