proposition: Lemma filter_mapsto f m (Hf : Proper (K.eq==>eq==>eq) f) k v : MapsTo k v (filter f m) <-> MapsTo k v m /\ f k v = true.
proof: Proof. rewrite <- bindings_spec1, filter_spec0, filter_InA, bindings_spec1. easy. intros (?,?) (?,?) (?,?); now apply Hf. Qed.
imports: Coq(Bool BinPos Pnat Setoid SetoidList PeanoNat) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)