Symbolic rules for SET.in

[ttuegel]

We should implement a symbolic rule for SET.in like the corresponding rule for MAP.in_keys:

\equals(false, X in [Y₁ Y₂ ...]) => \not \equal(X, Y₁) ∧ \not \equal (X, Y₂) ∧ ...

This should be easier for the external solver to reason about, but it will also help internal performance by breaking the predicate down into "atomic" forms. It also exposes X to unification with the Yᵢs.

[ttuegel]

Test cases:

\equals(false, X in []) = \top
\equals(false, X in [Y]) = \not \equals(X, Y)
\equals(false, X in [Y Z]) = \not \equals(X, Y) \and \not \equals(X, Z) \and \ceil([Y Z])
\equals(false, f(X) in [Y]) = \not \equals(f(X), Y) \and \ceil(f(X))