Commit 2022-07-23 17:07 4050b906

refactor(data/set/countable): golf using _root_.countable, review API (#15624)

• add set.countable_coe_iff, set.countable.to_subtype, set.to_countable, set.countable_univ, countable.to_set, set.countable.exists_surjective;
• generalize some lemmas from [encodable] to [countable];
• move section enumerate up to use it in countable_iff_exists_subset_range;
• golf some proofs using facts about _root_.countable;
• drop countable_encodable and countable_encodable', use set.to_countable instead.