contrapose
hucnt : ¬Set.Countable ({0, 1} ×ˢ Set.univ)
α : Type
s : Set α
⊢ ¬Set.Countable s → Set.Infinite s
hucnt : ¬Set.Countable ({0, 1} ×ˢ Set.univ)
α : Type
s : Set α
⊢ ¬Set.Infinite s → ¬¬Set.Countable s