proposition: Lemma mapi_1bis : forall m x e (f:key->elt->elt'), (forall x y e, E.eq x y -> f x e = f y e) -> MapsTo x e m -> MapsTo x (f x e) (mapi f m).
proof: Proof. intros. destruct (mapi_1 f H0) as (y,(H1,H2)). replace (f x e) with (f y e) by auto. auto. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface