WyCS: Added more test cases for #423.

I thought of a few more useful test cases which relate to #423.
Currently they are not passing, though ideally they would be.  There
appears to be a missing rule in the verifier for this case.
WyCS: Added Solver Rule for #423.

This rule handles the case where x contains y and y contains x, so x ==
y.
WyC: Minor tweak for consistent error reporting.

In adding the assert block, the way that failing assertions were
reported was different, and this was causing the regression tests to
fail.