* see dependencies *

In [1]:

```
import proveit
from proveit.logic.sets.inclusion import subset_eq_def
%proving fold_subset_eq
```

In [2]:

```
subset_eq_def
```

In [3]:

```
subset_eq_def_inst = subset_eq_def.instantiate()
```

In [4]:

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

In [5]:

```
%qed
```

Out[5]: