Prop-valued encodable

Stream: general

[Yury G. Kudryashov]

I think that we need a Prop-valued version of docs#encodable. The main reason for me is that we'll be able to have an instance from [fintype α] to [prop_encodable α] (of course, we need a better name).

[Yury G. Kudryashov]

And most lemmas about countable unions etc should take this new class as an argument.

[Kevin Buzzard]

is_countable?

[Yury G. Kudryashov]

Or countable with set.countable made protected.

[Yury G. Kudryashov]

(we have this for set.subsingleton and set.nonempty)

[Eric Wieser]

Could we rename encodable to has_encoding to free up the first name?

[Eric Wieser]

I guess countable is better to mathematicians anyway