proposition: Lemma mapi_2 : forall (elt elt':Type)(m: t elt)(x:key)(f:key->elt->elt'), In x (mapi f m) -> In x m.
proof: Proof. intros. apply mem_2. rewrite mem_find. destruct H as (v,H). generalize (find_1 H); clear H; intros. rewrite gmapi in H. destruct (find x m); auto. simpl in *; discriminate. Qed.
imports: Bool OrderedType ZArith OrderedType OrderedTypeEx FMapInterface