All countable types are small.

That is, any countable type is equivalent to a type in any universe.

@[instance 100]

instance Countable.toSmall (α : Type v) [Countable α] : Small.{w, v} α

theorem Uncountable.of_not_small {α : Type v} (h : ¬Small.{w, v} α) : Uncountable α