proposition: Lemma filter_incompatible : forall A B (IB:Inhab B) (f1 f2:A->B->Prop) M, (forall x y, x \indom M -> y = M[x] -> f1 x y -> f2 x y -> False) -> filter f1 (filter f2 M) = empty.
proof: Proof. Proof using. introv R. applys filter_none. intros k Hk Hf1. lets (Hk'&Hf2&E): indom_filter_inv Hk. rewrite* read_filter in Hf1. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOption LibRelation LibLogic LibOperation LibEpsilon LibMonoid LibSet)