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