WyCS: added rule for inferring equations.
This rule was preexisting, but commented out because it was previously
causing some kind of infinite loop.  However, it seems to work fine now
and potentially could improve the range of verification.