proposition: Lemma mapi_inv : forall m x b (f : key -> elt -> elt'), MapsTo x b (mapi f m) -> exists a y, E.eq y x /\ b = f y a /\ MapsTo x a m.
proof: Proof. intros; case_eq (find x m); intros. - exists e. destruct (@mapi_1 _ _ m x e f) as (y,(H1,H2)). + apply find_2; auto with map. + exists y; repeat split; auto with map. apply (MapsTo_fun (m:=mapi f m) (x:=x)); auto with map. - assert (In x (mapi f m)) by (exists b; auto). destruct (mapi_2 H1) as (a,H2). rewrite (find_1 H2) in H0; discriminate. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface