proposition: Lemma partition_iff_2 : forall m m2 k e, m2 = snd (partition f m) -> (MapsTo k e m2 <-> MapsTo k e m /\ f k e = false).
proof: Proof. unfold partition; simpl; intros. subst m2. rewrite filter_iff. - split; intros (H,H'); split; auto. + destruct (f k e); simpl in *; auto. + rewrite H'; auto. - repeat red; intros. f_equal. apply Hf; auto. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface