proposition: Lemma read_filter : forall A B (IB:Inhab B) (f:A->B->Prop) M x, x \indom M -> f x (M[x]) -> (filter f M)[x] = M[x].
proof: Proof. Proof using. introv Hx. lets Hx': indom_inv_app_neq_none (rm Hx). unfold filter. simpls. unfolds read_impl. destruct (M x); auto_false. case_if*. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOption LibRelation LibLogic LibOperation LibEpsilon LibMonoid LibSet)