* see dependencies *

In [1]:

```
import proveit
from proveit import x, S
from proveit.logic.sets.membership import not_in_set_def
theory = proveit.Theory() # the theorem's theory
```

In [2]:

```
%proving fold_not_in_set
```

In [3]:

```
not_in_set_def
```

In [4]:

```
not_in_set_def_spec = not_in_set_def.instantiate({x:x, S:S})
```

In [5]:

```
not_in_set_def_spec.derive_left_via_equality(assumptions=[not_in_set_def_spec.rhs])
```

In [6]:

```
%qed
```

Out[6]: