proposition: Lemma filter_iff (f : key -> elt -> bool) : Proper (K.eq==>eq==>eq) f -> forall m k e, MapsTo k e (filter f m) <-> MapsTo k e m /\ f k e = true.
proof: Proof. intros E m k e. rewrite <- !bindings_spec1, filter_spec, !InA_alt. setoid_rewrite filter_In. firstorder. - destruct x as (k',e'); simpl in *; subst. rewrite E; eauto. - destruct x as (k',e'); simpl in *; subst. exists (k',e'). split. easy. split; auto. rewrite <- E; eauto. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)