proposition: Lemma mapi_in_iff : forall m x (f:key->elt->elt'), In x (mapi f m) <-> In x m.
proof: Proof. split; intros; eauto with map. destruct H as (a,H). destruct (mapi_1 f H) as (y,(H0,H1)). exists (f y a); auto. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface