rcases hcnt with ⟨⟨f, finj⟩⟩
hun : {0, 1} = {0} ∪ {1}
hcnt : (∃ f, Function.Injective f) ∧ ∃ f, Function.Injective f
⊢ False
case intro.intro
hun : {0, 1} = {0} ∪ {1}
right✝ : ∃ f, Function.Injective f
f : ↑({0} ×ˢ Set.univ) → ℕ
finj : Function.Injective f
⊢ False