It is not related to KindSE

To save some work.

That simplifies the presentation and does not hurt.

We do not return Frames anymore

elem is not defined

We did not properly checked the O_l sets and thus always
returned only the set without any extensions from O_l.

+ a few comments

These may not be valid

Store just a sequence of sets and their union.
In the future, we'll store also an incremental solver
for fast queries about sequences.

This reverts commit 4cb07686.

Not only if  we give up extending it or we prove it is safe.
This way, we store all sequences that we ever create.

This reverts commit 62d66147.

That commit breaks things, we need to solve it better.

Do not keep those that are surely unreachable.

Concrete bool has not rewrite_and_simplify() method.

We must substract 1.

A step to soundness again.

And infer more of them.

We can reduce only equalities atm...

We cannot rewrite exprs with assuming exprs...

This reverts commit 0d4254eb.
This was wrong, it worked well.

We didn't finish the lhs transformation before
replacing the rest of the formula.