proposition: Lemma finite_remove : forall A B (M : map A B) (E : set A), finite M -> finite (M \- E).
proof: Proof. Proof using. introv. unfold finite. rewrite dom_remove. apply finite_remove. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOption LibRelation LibLogic LibOperation LibEpsilon LibMonoid LibSet)