proposition: Lemma union_finite : forall U V : set A, finite U -> finite V -> finite (union U V).
proof: Proof. Proof using. introv [L1 E1] [L2 E2]. exists (L1 ++ L2). intros x. rewrite in_union_eq. rewrite mem_app_eq. introv [H|H]; auto. Qed.
imports: TLC(LibTactics LibList) TLC(LibSet LibLogic LibEqual LibReflect)