countable_split
⊢ ∀X f m. INJ f X 𝕌(:num list # α list) ∧ (∀x y. x ∈ X ∧ MEM y (SND (f x)) ⇒ y ∈ X ∧ m y < m x) ⇒ countable X
list_countable
⊢ countable Lset ⇔ countable (BIGUNION (IMAGE set Lset))
unit_countable
⊢ countable 𝕌(:unit)