Distinguish stuck proof states

[ttuegel]

Proof states can get "stuck" for two reasons:

1. The terms of the left- and right-hand sides do not unify, and the left-hand side cannot be rewritten any further.
2. The left- and right-hand side are unifiable, but the left-hand side condition does not imply the right-hand side condition.

---

• Store this information in the execution graph.
• Emit a different warning type for each case.
• Present this information in kore-repl.

[ttuegel]

I don't intend for us to take on this whole task at once, but at least we can implement Emit a different warning type for each case.