proposition: Lemma filter_idempotent : forall A B (IB:Inhab B) (f:A->B->Prop) M, filter f (filter f M) = filter f M.
proof: Proof. Proof using. introv IB. symmetry. applys extensionality. { intros k. repeat rewrite (@indom_filter_eq A B IB). iff* (Hk&Hfk). { split*. rewrite* read_filter. } } { intros k Hk. lets (?&?&?): indom_filter_inv Hk. repeat rewrite* read_filter. } Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOption LibRelation LibLogic LibOperation LibEpsilon LibMonoid LibSet)