PR #16965: feat(data/{finset,set}/basic): A nonempty set ...

Stream: triage

[Random Issue Bot]

Today I chose PR 16965 for discussion!

feat(data/{finset,set}/basic): A nonempty set of a subsingleton is univ
Created by @Yaël Dillies (@YaelDillies) on 2022-10-13
Labels: awaiting-review

Is this PR still relevant? Any recent updates? Anyone making progress?

[Yaël Dillies]

Mergeable in my opinion.