proposition: Lemma mapi_o : forall m x (f:key->elt->elt'), (forall x y e, E.eq x y -> f x e = f y e) -> find x (mapi f m) = Datatypes.option_map (f x) (find x m).
proof: Proof. intros. generalize (find_mapsto_iff (mapi f m) x) (find_mapsto_iff m x) (fun b => mapi_mapsto_iff m x b H). destruct (find x (mapi f m)); destruct (find x m); simpl; auto; intros. - rewrite <- H0; rewrite H2; exists e0; rewrite H1; auto. - destruct (H0 e) as [_ H3]. rewrite H2 in H3. destruct H3 as (a,(_,H3)); auto. rewrite H1 in H3; discriminate. - rewrite <- H0; rewrite H2; exists e; rewrite H1; auto. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface