Commit 2020-10-04 11:10 e8b65e68

feat(data/set/basic): eq_singleton_iff_unique_mem (#4387) We have this lemma for finset. Add a version for set (with the same name).