proposition: Lemma map_o : forall m x (f:elt->elt'), find x (map f m) = Datatypes.option_map f (find x m).
proof: Proof. intros. generalize (find_mapsto_iff (map f m) x) (find_mapsto_iff m x) (fun b => map_mapsto_iff m x b f). destruct (find x (map f m)); destruct (find x m); simpl; auto; intros. - rewrite <- H; rewrite H1; exists e0; rewrite H0; auto. - destruct (H e) as [_ H2]. rewrite H1 in H2. destruct H2 as (a,(_,H2)); auto. rewrite H0 in H2; discriminate. - rewrite <- H; rewrite H1; exists e; rewrite H0; auto. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface