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 elt elt' m; exact (@Raw.mapi_1 elt elt' (this m)). Qed.
imports: FMapInterface