proposition: Lemma set_finite_union s s' : set_finite (s ∪₁ s') <-> set_finite s /\ set_finite s'.
proof: Proof. u; split; splits; ins; desf; eauto. eexists (_ ++ _); ins; desf; eauto using in_or_app. Qed.
imports: HahnBase Program.Basics List Arith micromega.Lia Relations Setoid Morphisms