Remove Defined markers in simplifyConjunctionByAssumption

[ana-pantilie]

Needs #2366

Until #2351 is done, this will fix those cases where a conjunction isn't simplified correctly because the terms differ by Defined markers.

---

Review checklist

The author performs the actions on the checklist. The reviewer evaluates the work and checks the boxes as they are completed.

• Summary. Write a summary of the changes. Explain what you did to fix the issue, and why you did it. Present the changes in a logical order. Instead of writing a summary in the pull request, you may push a clean Git history.
• Documentation. Write documentation for new functions. Update documentation for functions that changed, or complete documentation where it is missing.
• Tests. Write unit tests for every change. Write the unit tests that were missing before the changes. Include any examples from the reported issue as integration tests.
• Clean up. The changes are already clean. Clean up anything near the changes that you noticed while working. This does not mean only spatially near the changes, but logically near: any code that interacts with the changes!

[ttuegel]

What is the difference between Right fg and Left fg?

[ana-pantilie]

Right fg will apply mkDefined to the f(g(x) in the second equals, and Left fg to the one in the first. This makes sure we test that the Defined markers are removed when both assuming and looking up terms.

[ttuegel]

Using definedFg here actually requires that eitherFunc is Right fg or Left fg, so I would rather we not allow passing in any value there.

[ana-pantilie]

Do you mean we should remove definedFg from condition? Edit: I think this is what you meant by this comment, so I pushed a commit with this change. If you think something else should change, let me know.