This closes issue #49 (closed). Some remarks:
- It's called
TopSet, which corresponds with
- We now have a generic
Hint Resolve coPset_top_subseteq : coreno longer works because the lemma is generic in a type class. AFAIK it is only used for
solve_ndisjoint, so I added a specialized version to the
ndisjhint database. We already have specialized versions of other set lemmas there.