proposition: Lemma set_finite_bunion s (F: set_finite s) ss : set_finite (set_bunion s ss) <-> forall a (COND: s a), set_finite (ss a).
proof: Proof. u; split; ins; desf; eauto. revert s F H; induction findom; ins. by exists nil; ins; desf; eauto. specialize (IHfindom (fun x => s x /\ x <> a)); ins. specialize_full IHfindom; ins; desf; eauto. by apply F in IN; desf; eauto. tertium_non_datur (s a) as [X|X]. eapply H in X; desf. eexists (findom0 ++ findom1); ins; desf. tertium_non_datur (y = a); desf; eauto 8 using in_or_app. eexists findom0; ins; desf; apply IHfindom; eexists; splits; eauto; congruence. Qed.
imports: HahnBase Program.Basics List Arith micromega.Lia Relations Setoid Morphisms