have hun : ({0, 1} : Set ℕ) = {0} ∪ {1} := by
  rw [Set.union_comm, Set.union_singleton]
hcnt : Set.Countable ({0, 1} ×ˢ Set.univ)
⊢ False
hcnt : Set.Countable ({0, 1} ×ˢ Set.univ)
hun : {0, 1} = {0} ∪ {1}
⊢ False