proposition: Lemma indom_filter_eq : forall A B (IB:Inhab B) (f:A->B->Prop) M x, x \indom (filter f M) = (x \indom M /\ f x (M[x])).
proof: Proof. Proof using. intros. simpl. unfold dom_impl, filter, read_impl. rew_set. extens. destruct* (M x). { case_if; auto_false*. } Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOption LibRelation LibLogic LibOperation LibEpsilon LibMonoid LibSet)