Check equality of expressions up to convertibility

[oskgo]

This was already being done when checking equality of instructions and statements, but not expressions.

It seems like this was an accident. The EqTest module exposes the for_expr definition used by the internal EqTest_base while defining its own that ends up being used by for_instr and for_stmt. The relevant line number is 1896.

It's likely that this will break something, but I don't have an example. I found this while trying to fix #990, but AFAICT this change won't break any uses of sim by itself. See also #997.

[oskgo]

On further investigation, this is unlikely to be breaking. It makes byupto stronger, but since byupto always closes goals that won't be breaking.

I haven't looked into whether other code uses EqTest.for_expr, but an earlier iteration of this PR broke EqTest.for_expr but only ended up failing CI tests for byupto.