proposition: Lemma filter_all : forall A B (IB:Inhab B) (f:A->B->Prop) M, (forall x, x \indom M -> f x (M[x])) -> filter f M = M.
proof: Proof. Proof using. introv H. symmetry. applys extensionality. { intros k. rewrite (@indom_filter_eq A B IB). iff*. } { intros k Hk. rewrite* read_filter. } Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOption LibRelation LibLogic LibOperation LibEpsilon LibMonoid LibSet)