# [isabelle] Trying to reduce equality proofs from 2 to 1 step

```Hi,

```
I've set up a bunch of simp rules, and I'm getting lots of 1 step proofs with "by(simp)".
```
```
However, there's one common proof which I can't figure out how to get in 1 step, which is set equality for the case where I have to prove "A is a subset of B and B is a subset of A", which I have to do because the auto provers can't prove "A = B" directly.
```
```
The problem is that my "A is a subset of B and B is a subset of A" is my main equality "A=B", so I'm blank on how I can automate the connection between the two.
```
```
I attach a PDF. On page 7, Notation 3.1.10, I create an abbreviation for "A is a subset of B and B is a subset of A". On page 8 is my Theorem 3.1.12 which shows that "A is a subset of B and B is a subset of A" is equivalent to "A=B".
```
```
My theory is filling up with proofs to theorems in which I state a proof step with my "equal subsets" operator, prove it with "by(simp)", and then have to finish it off with the Theorem 3.1.12.
```
```
Starting on page 37, there's 6 out of 7 theorems where I do that. Then on page 39, there's the examples that show how I can get equality with my "equal subsets" operator, but not with the normal "=".
```
```
That's related to the main reason I care, which is that I'd like to show finite set equality using only one automatic proof method command.
```
If anyone can tell me how to do that, I'd appreciate it.

Regards,
GB

```

Attachment: sTs_doc.pdf