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