feat(logic/basic): subsingleton_of_not_nonempty (#7043)
feat(logic/basic): subsingleton_of_not_nonempty (#7043)

Also generalize `not_nonempty_iff_imp_false` to `Sort *`.





leanprover-community/mathlib,leanprover-community/mathlib