proposition: Lemma set_finite_unionI s (F: set_finite s) s' (F': set_finite s') : set_finite (s ∪₁ s').
proof: Proof. u; desf; eauto; eexists (_ ++ _); ins; desf; eauto using in_or_app. Qed.
imports: HahnBase Program.Basics List Arith micromega.Lia Relations Setoid Morphisms