simp only [Set.mem_singleton_iff, Set.not_infinite, not_not, Set.Finite.countable]
hucnt : ¬Set.Countable ({0, 1} ×ˢ Set.univ)
α : Type
s : Set α
⊢ ¬Set.Infinite s → ¬¬Set.Countable s
hucnt : ¬Set.Countable ({0, 1} ×ˢ Set.univ)
α : Type
s : Set α
⊢ Set.Finite s → Set.Countable s