proposition: Lemma finite_union_eq : forall E F, finite (E \u F) = (finite E /\ finite F).
proof: Proof. Proof using. extens. iff. applys* finite_union_inv. applys* finite_union. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibList LibOperation LibMonoid LibInt LibNat LibEpsilon LibRelation LibMin)