proposition: Lemma indom_filter_inv : forall A B (IB:Inhab B) (f:A->B->Prop) M x, x \indom (filter f M) -> x \indom M /\ f x (M[x]) /\ (filter f M)[x] = M[x].
proof: Proof. Proof using. introv H. hint read_filter. rewrite* (@indom_filter_eq A B IB) in H. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOption LibRelation LibLogic LibOperation LibEpsilon LibMonoid LibSet)