proposition: Lemma mapi_1 : forall (m:t elt)(x:key)(e:elt)(f:key->elt->elt'), MapsTo x e m -> exists y, X.eq y x /\ MapsTo x (f y e) (mapi f m).
proof: Proof. intros m x e f. induction m. - inversion 1. - destruct a as (x',e'). simpl. inversion_clear 1. + exists x'. destruct H0; simpl in *. split. * auto with ordered_type. * constructor 1. unfold eqke in *; simpl in *; intuition congruence. + destruct IHm as (y, hyp); auto. exists y; intuition auto with ordered_type. Qed.
imports: FMapInterface