have hncnt {α : Type} {s : Set α}
  : ¬Set.Countable s → Set.Infinite s := by
  contrapose
  simp only [Set.mem_singleton_iff, Set.not_infinite, not_not, Set.Finite.countable]
  exact Set.Finite.countable
case right
hucnt : ¬Set.Countable ({0, 1} ×ˢ Set.univ)
⊢ Set.Infinite ({0, 1} ×ˢ Set.univ)
case right
hucnt : ¬Set.Countable ({0, 1} ×ˢ Set.univ)
hncnt : ∀ {α : Type} {s : Set α}, ¬Set.Countable s → Set.Infinite s
⊢ Set.Infinite ({0, 1} ×ˢ Set.univ)