Improve simplifications

[Yag000]

I've added a few more improvement to the simplifications:

These new rules:

$$\text {if } \phi \preccurlyeq \psi \text { then } \phi \implies \psi \equiv \top$$ $$\text {if } \phi \preccurlyeq \bot \text { then } \phi \implies \psi \equiv \top$$ $$\text {if } \top \preccurlyeq \psi \text { then } \phi \implies \psi \equiv \top$$ $$\text {if } \top \preccurlyeq \phi \text { then } \phi \implies \psi \equiv \psi$$ $$\text {if } \psi \preccurlyeq \bot \text { then } \phi \implies \psi \equiv \neg\phi$$

And obviously_smaller now looks in disjunctions and conjunctions recursively to find if one is smaller than the other.