feat(logic/encodable/basic): an encodable type is countable (#15524)
feat(logic/encodable/basic): an encodable type is countable (#15524)

Also simplify `nonempty (encodable X)` to `countable X`.





leanprover-community/mathlib,leanprover-community/mathlib