fact: Definition coGset_to_top_set `{Countable A, Empty C, Singleton A C, Union C, Top C, Difference C} (X : coGset A) : C := match X with | FinGSet X => list_to_set (elements X) | CoFinGset X => ⊤ ∖ list_to_set (elements X) end.
imports: stdpp(decidable finite gmap coPset) stdpp(options)