Define equivalence of formulas

[eionblanc]

We say that two formulas are equivalent (w.r.t. a given structure) if their interpretations define the same set (there are a few equivalent definitions; I think this one is most straightforward for our purposes). This will give our notion of definable sets more utility once we have that established.

In Lean, we will take the sets defined by two formulas and check whether or not they contain exactly the same elements from the universe.