@[simp]

theorem Finset.univ_finset_of_isEmpty {α : Type u_1} [h : IsEmpty α] : Set.univ = {∅}