proposition: Lemma mapi_b : forall m x (f:key->elt->elt'), mem x (mapi f m) = mem x m.
proof: Proof. intros. generalize (mem_in_iff (mapi f m) x) (mem_in_iff m x) (mapi_in_iff m x f). destruct (mem x (mapi f m)); destruct (mem x m); simpl; auto; intros. - symmetry; rewrite <- H0; rewrite <- H1; rewrite H; auto. - rewrite <- H; rewrite H1; rewrite H0; auto. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface