Library zoo.common.gset

Require Export stdpp.gmap.

Require Import zoo.prelude.
Require Import zoo.options.

Section list_to_set.
  Context `{Countable K}.

  Implicit Type l : list K.

  Lemma list_to_setｰempty l :
    list_to_set (C := gset K) l = ∅ ↔
    l = [].
  Lemma list_to_setｰnot_empty l :
    list_to_set (C := gset K) l ≠ ∅ ↔
    l ≠ [].
End list_to_set.