proposition: Lemma partition_iff_1 : forall m m1 k e, m1 = fst (partition f m) -> (MapsTo k e m1 <-> MapsTo k e m /\ f k e = true).
proof: Proof. unfold partition; simpl; intros. subst m1. apply filter_iff; auto. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface