proposition: Lemma map_1 : forall (m:t elt)(x:key)(e:elt)(f:elt->elt'), MapsTo x e m -> MapsTo x (f e) (map f m).
proof: Proof. intros m x e f. induction m. - inversion 1. - destruct a as (x',e'). simpl. inversion_clear 1. + constructor 1. unfold eqke in *; simpl in *; intuition congruence. + constructor 2. unfold MapsTo in *; auto. Qed.
imports: FMapInterface