proposition: Lemma finite_remove : forall E F, finite E -> finite (E \- F).
proof: Proof. Proof using. introv HE. apply finite_of_ex_list_covers. lets (L&EQ): finite_inv_list_covers HE. unfold list_covers. set_unf. exists* L. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibList LibOperation LibMonoid LibInt LibNat LibEpsilon LibRelation LibMin)