proposition: Lemma dom_filter : forall A B (IB:Inhab B) (f:A->B->Prop) M, dom (filter f M) \c dom M.
proof: Proof. Proof using. intros. simpl. unfold dom_impl, filter. rew_set. intros x. rew_set. destruct* (M x). Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOption LibRelation LibLogic LibOperation LibEpsilon LibMonoid LibSet)