proposition: Lemma filter_none : forall A B (IB:Inhab B) (f:A->B->Prop) M, (forall x, x \indom M -> ~ f x (M[x])) -> filter f M = empty.
proof: Proof. Proof using. introv H. symmetry. applys extensionality. { intros k. rewrite dom_empty. rew_set. iff R; tryfalse. forwards* (Hk&Hfk&_): indom_filter_inv R. } { intros k. rewrite dom_empty. rew_set. auto_false. } Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOption LibRelation LibLogic LibOperation LibEpsilon LibMonoid LibSet)