proposition: Lemma map_2 : forall (elt elt':Type)(m: t elt)(x:key)(f:elt->elt'), In x (map f m) -> In x m.
proof: Proof. intros; unfold map in *; eapply mapi_2; eauto. Qed.
imports: Bool OrderedType ZArith OrderedType OrderedTypeEx FMapInterface