* see dependencies *

In [1]:

```
import proveit
from proveit import defaults
from proveit import x, y
from proveit.logic import NotEquals, Not, Equals, TRUE, FALSE, InSet, NotInSet, Set
from proveit.logic.equality import not_equals_def
from proveit.logic.equality import sub_right_side_into
from proveit.logic.sets.enumeration import not_in_singleton_equiv, in_singleton_eval_true, singleton_def
%proving in_singleton_eval_false
```

In [2]:

```
defaults.assumptions = in_singleton_eval_false.conditions
```

In [3]:

```
step1 = not_equals_def.instantiate({x:x, y:y})
```

In [4]:

```
state1 = Equals(NotEquals(x,y), TRUE).prove()
```

In [5]:

```
step1.sub_right_side_into(state1)
```

In [6]:

```
state2 = Equals(Equals(x,y), FALSE).prove()
```

In [7]:

```
state3 = singleton_def.instantiate({x:x, y:y})
```

In [8]:

```
goal = state3.sub_left_side_into(state2)
```

In [9]:

```
goal.generalize([x,y], conditions = in_singleton_eval_false.conditions)
```

In [10]:

```
%qed
```

Out[10]: