WyCS: Bug fix for normalising polynomials.
The problem was that I was normalising polynomials whilst ignoring their
context.  This is not safe if, for example, you factor a polynomial on
one side of an equals statement.  In such case, it doesn't work.
WyCS: Added another failing test case.
This test case is failing, apparently because quantifier instantiation
is not being triggered.  I'm not sure how this is possibler!?