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