proposition: Lemma mapi_2 : forall (m:t elt)(x:key)(f:key->elt->elt'), In x (mapi f m) -> In x m.
proof: Proof. intros m x f. induction m; simpl. - intros (e,abs). inversion abs. - destruct a as (x',e). intros hyp. inversion hyp. clear hyp. inversion H; subst; rename x0 into e'. + exists e; constructor. unfold eqke in *; simpl in *; intuition. + destruct IHm as (e'',hyp). * exists e'; auto. * exists e''. constructor 2; auto. Qed.
imports: FMapInterface