proposition: Lemma map_mapsto_iff : forall m x b (f : elt -> elt'), MapsTo x b (map f m) <-> exists a, b = f a /\ MapsTo x a m.
proof: Proof. split. - case_eq (find x m); intros. + exists e. split. * apply (MapsTo_fun (m:=map f m) (x:=x)); auto with map. * apply find_2; auto with map. + assert (In x (map f m)) by (exists b; auto). destruct (map_2 H1) as (a,H2). rewrite (find_1 H2) in H; discriminate. - intros (a,(H,H0)). subst b; auto with map. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface