proposition: Lemma mapi_1 : forall (elt elt':Type)(m: t elt)(x:key)(e:elt)(f:key->elt->elt'), MapsTo x e m -> exists y, E.eq y x /\ MapsTo x (f y e) (mapi f m).
proof: Proof. intros. exists x. split; [red; auto|]. apply find_2. generalize (find_1 H); clear H; intros. rewrite gmapi. rewrite H. simpl; auto. Qed.
imports: Bool OrderedType ZArith OrderedType OrderedTypeEx FMapInterface