proposition: Lemma mapi_mapsto_iff : forall m x b (f:key->elt->elt'), (forall x y e, E.eq x y -> f x e = f y e) -> (MapsTo x b (mapi f m) <-> exists a, b = f x a /\ MapsTo x a m).
proof: Proof. split. - intros. destruct (mapi_inv H0) as (a,(y,(H1,(H2,H3)))). exists a; split; auto. subst b; auto. - intros (a,(H0,H1)). subst b. apply mapi_1bis; auto. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface