proposition: Lemma finite_union_eq P Q : finite (union P Q) <-> finite P /\ finite Q.
proof: Proof. split. 2: intros [P_fin Q_fin]; apply finite_union; hyp. revert P Q. cut (forall P Q, finite (union P Q) -> finite P). intros L P Q PUQ_fin. split; eapply L. apply PUQ_fin. rewrite union_com. apply PUQ_fin. intros P Q. rewrite !finite_eq. intros [l hl]. ex (select (dec1 P) l). intro x. split. intro xP. hnf. apply select_complete; fo. intro xPl. hnf in xPl. apply select_correct in xPl. fo. Qed.
imports: Coq(Basics Morphisms Setoid) CoLoR(ClassicUtil IotaUtil EpsilonUtil LogicUtil NatUtil FunUtil ListUtil ListNodup SetUtil BoundNat)