proposition: Lemma dom_remove : forall A B (M : map A B) (E : set A), dom (M \- E) = dom M \- E.
proof: Proof. Proof using. intros. simpl. unfold dom_impl, remove_impl. rew_set. intros x. rew_set. iff R; case_if*. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOption LibRelation LibLogic LibOperation LibEpsilon LibMonoid LibSet)