In [1]:

```
import proveit
# Prepare this notebook for defining the axioms of a theory:
%axioms_notebook # Keep this at the top following 'import proveit'.
from proveit import n, x
from proveit.logic import Forall, Equals, InSet, Set, EmptySet
from proveit.core_expr_types import y_1_to_n
from proveit.logic.sets import x_equals_any_y
from proveit.numbers import Natural
%begin axioms
```

**Membership in an enumeration is the same as being equal to any of the contents of the enumeration:**

In [2]:

```
enum_set_def = Forall(n, Forall((x, y_1_to_n),
Equals(InSet(x, Set(y_1_to_n)),
x_equals_any_y).with_wrapping_at(2)),
domain=Natural)
```

**Define the empty set as an enumerated set with no elements.**

In [3]:

```
empty_set_def = Equals(EmptySet, Set())
```

In [4]:

```
#
# might need an axiom here:
# if 2 enum sets are SetEquiv then they are equal
# see some hard-copy notes/comments from project meeting 2/07/2020
```

In [ ]:

```
```

In [5]:

```
%end axioms
```