proposition: Lemma finite_union : forall E F, finite E -> finite F -> finite (E \u F).
proof: Proof. Proof using. introv H1 H2. apply finite_of_ex_list_covers. lets (L1&E1): finite_inv_list_covers H1. lets (L2&E2): finite_inv_list_covers H2. exists (L1++L2). unfolds list_covers. introv M. rewrite @in_union_eq in M; try typeclass. rewrite* mem_app_eq. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibList LibOperation LibMonoid LibInt LibNat LibEpsilon LibRelation LibMin)