proposition: Lemma finite_union_inv : forall E F, finite (E \u F) -> finite E /\ finite F.
proof: Proof. Proof using. introv H. lets (L&HL): finite_inv_list_covers H. split. { apply finite_of_ex_list_covers. exists L. unfolds list_covers. intros x M. applys HL. apply in_union_l. auto. } { apply finite_of_ex_list_covers. exists L. unfolds list_covers. intros x M. applys HL. apply in_union_r. auto. } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibList LibOperation LibMonoid LibInt LibNat LibEpsilon LibRelation LibMin)