proposition: Lemma union_finite X Y : set_finite X → set_finite Y → set_finite (X ∪ Y).
proof: Proof. intros [lX ?] [lY ?]; exists (lX ++ lY); intros x. rewrite elem_of_union, elem_of_app; naive_solver. Qed.
imports: stdpp(finite) stdpp(options)