rcases hcntiA with ⟨hcntA, _⟩
α : Type
A B : Set α
hsub : A ⊆ B
hcntiA : Countably_Infinite A
hucnt : Uncountable B
⊢ Uncountable (B \ A)
case intro
α : Type
A B : Set α
hsub : A ⊆ B
hucnt : Uncountable B
hcntA : Set.Countable A
right✝ : Set.Infinite A
⊢ Uncountable (B \ A)