This patch fixes several bugs in the handling of impliciation
constraints, thereby fixing several regression-suite failures.

On the way I managed to further simplify the code in TcSimplify;
the extra lines are comments.